H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 17.226 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ CR

mainModule List

((sort :: [Ratio Int] -> [Ratio Int]) :: [Ratio Int] -> [Ratio Int])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge

cmp xs []

merge

cmp [] ys

merge

cmp (x : xs) (y : ys)

case	x `cmp` y of
	GT	->	y : merge cmp (x : xs) ys
	_	->	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Case Reductions:
The following Case expression

case cmp x y of
GT → y : merge cmp (x : xs) ys

_ → x : merge cmp xs (y : ys)

is transformed to

merge0 y cmp x xs ys GT = y : merge cmp (x : xs) ys

merge0 y cmp x xs ys _ = x : merge cmp xs (y : ys)

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

mainModule List

((sort :: [Ratio Int] -> [Ratio Int]) :: [Ratio Int] -> [Ratio Int])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((sort :: [Ratio Int] -> [Ratio Int]) :: [Ratio Int] -> [Ratio Int])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule List

(sort :: [Ratio Int] -> [Ratio Int])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="sort",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="sort vz3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="mergesort compare vz3",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="(mergesort' compare) . map wrap",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="mergesort' compare (map wrap vz3)",fontsize=16,color="burlywood",shape="box"];16080[label="vz3/vz30 : vz31",fontsize=10,color="white",style="solid",shape="box"];6 -> 16080[label="",style="solid", color="burlywood", weight=9];
16080 -> 7[label="",style="solid", color="burlywood", weight=3];
16081[label="vz3/[]",fontsize=10,color="white",style="solid",shape="box"];6 -> 16081[label="",style="solid", color="burlywood", weight=9];
16081 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="mergesort' compare (map wrap (vz30 : vz31))",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="mergesort' compare (map wrap [])",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="mergesort' compare (wrap vz30 : map wrap vz31)",fontsize=16,color="burlywood",shape="box"];16082[label="vz31/vz310 : vz311",fontsize=10,color="white",style="solid",shape="box"];9 -> 16082[label="",style="solid", color="burlywood", weight=9];
16082 -> 11[label="",style="solid", color="burlywood", weight=3];
16083[label="vz31/[]",fontsize=10,color="white",style="solid",shape="box"];9 -> 16083[label="",style="solid", color="burlywood", weight=9];
16083 -> 12[label="",style="solid", color="burlywood", weight=3];
10[label="mergesort' compare []",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="mergesort' compare (wrap vz30 : map wrap (vz310 : vz311))",fontsize=16,color="black",shape="box"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="mergesort' compare (wrap vz30 : map wrap [])",fontsize=16,color="black",shape="box"];12 -> 15[label="",style="solid", color="black", weight=3];
13[label="[]",fontsize=16,color="green",shape="box"];14[label="mergesort' compare (wrap vz30 : wrap vz310 : map wrap vz311)",fontsize=16,color="black",shape="box"];14 -> 16[label="",style="solid", color="black", weight=3];
15[label="mergesort' compare (wrap vz30 : [])",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16[label="mergesort' compare (merge_pairs compare (wrap vz30 : wrap vz310 : map wrap vz311))",fontsize=16,color="black",shape="box"];16 -> 18[label="",style="solid", color="black", weight=3];
17[label="wrap vz30",fontsize=16,color="black",shape="triangle"];17 -> 19[label="",style="solid", color="black", weight=3];
18 -> 15606[label="",style="dashed", color="red", weight=0];
18[label="mergesort' compare (merge compare (wrap vz30) (wrap vz310) : merge_pairs compare (map wrap vz311))",fontsize=16,color="magenta"];18 -> 15607[label="",style="dashed", color="magenta", weight=3];
18 -> 15608[label="",style="dashed", color="magenta", weight=3];
19[label="vz30 : []",fontsize=16,color="green",shape="box"];15607 -> 15761[label="",style="dashed", color="red", weight=0];
15607[label="merge compare (wrap vz30) (wrap vz310)",fontsize=16,color="magenta"];15607 -> 15762[label="",style="dashed", color="magenta", weight=3];
15607 -> 15763[label="",style="dashed", color="magenta", weight=3];
15608[label="map wrap vz311",fontsize=16,color="burlywood",shape="triangle"];16086[label="vz311/vz3110 : vz3111",fontsize=10,color="white",style="solid",shape="box"];15608 -> 16086[label="",style="solid", color="burlywood", weight=9];
16086 -> 15764[label="",style="solid", color="burlywood", weight=3];
16087[label="vz311/[]",fontsize=10,color="white",style="solid",shape="box"];15608 -> 16087[label="",style="solid", color="burlywood", weight=9];
16087 -> 15765[label="",style="solid", color="burlywood", weight=3];
15606[label="mergesort' compare (vz501 : merge_pairs compare vz502)\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];16088[label="vz502/vz5020 : vz5021",fontsize=10,color="white",style="solid",shape="box"];15606 -> 16088[label="",style="solid", color="burlywood", weight=9];
16088 -> 15766[label="",style="solid", color="burlywood", weight=3];
16089[label="vz502/[]",fontsize=10,color="white",style="solid",shape="box"];15606 -> 16089[label="",style="solid", color="burlywood", weight=9];
16089 -> 15767[label="",style="solid", color="burlywood", weight=3];
15762 -> 17[label="",style="dashed", color="red", weight=0];
15762[label="wrap vz310",fontsize=16,color="magenta"];15762 -> 15768[label="",style="dashed", color="magenta", weight=3];
15763 -> 17[label="",style="dashed", color="red", weight=0];
15763[label="wrap vz30",fontsize=16,color="magenta"];15761[label="merge compare vz504 vz503",fontsize=16,color="burlywood",shape="triangle"];16092[label="vz503/vz5030 : vz5031",fontsize=10,color="white",style="solid",shape="box"];15761 -> 16092[label="",style="solid", color="burlywood", weight=9];
16092 -> 15769[label="",style="solid", color="burlywood", weight=3];
16093[label="vz503/[]",fontsize=10,color="white",style="solid",shape="box"];15761 -> 16093[label="",style="solid", color="burlywood", weight=9];
16093 -> 15770[label="",style="solid", color="burlywood", weight=3];
15764[label="map wrap (vz3110 : vz3111)",fontsize=16,color="black",shape="box"];15764 -> 15771[label="",style="solid", color="black", weight=3];
15765[label="map wrap []",fontsize=16,color="black",shape="box"];15765 -> 15772[label="",style="solid", color="black", weight=3];
15766[label="mergesort' compare (vz501 : merge_pairs compare (vz5020 : vz5021))\n  Ord a",fontsize=16,color="burlywood",shape="box"];16094[label="vz5021/vz50210 : vz50211",fontsize=10,color="white",style="solid",shape="box"];15766 -> 16094[label="",style="solid", color="burlywood", weight=9];
16094 -> 15773[label="",style="solid", color="burlywood", weight=3];
16095[label="vz5021/[]",fontsize=10,color="white",style="solid",shape="box"];15766 -> 16095[label="",style="solid", color="burlywood", weight=9];
16095 -> 15774[label="",style="solid", color="burlywood", weight=3];
15767[label="mergesort' compare (vz501 : merge_pairs compare [])\n  Ord a",fontsize=16,color="black",shape="box"];15767 -> 15775[label="",style="solid", color="black", weight=3];
15768[label="vz310",fontsize=16,color="green",shape="box"];15769[label="merge compare vz504 (vz5030 : vz5031)",fontsize=16,color="burlywood",shape="box"];16096[label="vz504/vz5040 : vz5041",fontsize=10,color="white",style="solid",shape="box"];15769 -> 16096[label="",style="solid", color="burlywood", weight=9];
16096 -> 15776[label="",style="solid", color="burlywood", weight=3];
16097[label="vz504/[]",fontsize=10,color="white",style="solid",shape="box"];15769 -> 16097[label="",style="solid", color="burlywood", weight=9];
16097 -> 15777[label="",style="solid", color="burlywood", weight=3];
15770[label="merge compare vz504 []",fontsize=16,color="black",shape="box"];15770 -> 15778[label="",style="solid", color="black", weight=3];
15771[label="wrap vz3110 : map wrap vz3111",fontsize=16,color="green",shape="box"];15771 -> 15779[label="",style="dashed", color="green", weight=3];
15771 -> 15780[label="",style="dashed", color="green", weight=3];
15772[label="[]",fontsize=16,color="green",shape="box"];15773[label="mergesort' compare (vz501 : merge_pairs compare (vz5020 : vz50210 : vz50211))\n  Ord a",fontsize=16,color="black",shape="box"];15773 -> 15781[label="",style="solid", color="black", weight=3];
15774[label="mergesort' compare (vz501 : merge_pairs compare (vz5020 : []))\n  Ord a",fontsize=16,color="black",shape="box"];15774 -> 15782[label="",style="solid", color="black", weight=3];
15775[label="mergesort' compare (vz501 : [])\n  Ord a",fontsize=16,color="black",shape="box"];15775 -> 15783[label="",style="solid", color="black", weight=3];
15776[label="merge compare (vz5040 : vz5041) (vz5030 : vz5031)",fontsize=16,color="black",shape="box"];15776 -> 15784[label="",style="solid", color="black", weight=3];
15777[label="merge compare [] (vz5030 : vz5031)",fontsize=16,color="black",shape="box"];15777 -> 15785[label="",style="solid", color="black", weight=3];
15778[label="vz504",fontsize=16,color="green",shape="box"];15779 -> 17[label="",style="dashed", color="red", weight=0];
15779[label="wrap vz3110",fontsize=16,color="magenta"];15779 -> 15786[label="",style="dashed", color="magenta", weight=3];
15780 -> 15608[label="",style="dashed", color="red", weight=0];
15780[label="map wrap vz3111",fontsize=16,color="magenta"];15780 -> 15787[label="",style="dashed", color="magenta", weight=3];
15781[label="mergesort' compare (vz501 : merge compare vz5020 vz50210 : merge_pairs compare vz50211)\n  Ord a",fontsize=16,color="black",shape="box"];15781 -> 15788[label="",style="solid", color="black", weight=3];
15782[label="mergesort' compare (vz501 : vz5020 : [])\n  Ord a",fontsize=16,color="black",shape="box"];15782 -> 15789[label="",style="solid", color="black", weight=3];
15783[label="vz501\n  Ord a",fontsize=16,color="green",shape="box"];15784 -> 15828[label="",style="dashed", color="red", weight=0];
15784[label="merge0 vz5030 compare vz5040 vz5041 vz5031 (compare vz5040 vz5030)",fontsize=16,color="magenta"];15784 -> 15829[label="",style="dashed", color="magenta", weight=3];
15784 -> 15830[label="",style="dashed", color="magenta", weight=3];
15784 -> 15831[label="",style="dashed", color="magenta", weight=3];
15784 -> 15832[label="",style="dashed", color="magenta", weight=3];
15784 -> 15833[label="",style="dashed", color="magenta", weight=3];
15785[label="vz5030 : vz5031",fontsize=16,color="green",shape="box"];15786[label="vz3110",fontsize=16,color="green",shape="box"];15787[label="vz3111",fontsize=16,color="green",shape="box"];15788[label="mergesort' compare (merge_pairs compare (vz501 : merge compare vz5020 vz50210 : merge_pairs compare vz50211))\n  Ord a",fontsize=16,color="black",shape="box"];15788 -> 15791[label="",style="solid", color="black", weight=3];
15789[label="mergesort' compare (merge_pairs compare (vz501 : vz5020 : []))\n  Ord a",fontsize=16,color="black",shape="box"];15789 -> 15792[label="",style="solid", color="black", weight=3];
15829[label="vz5040",fontsize=16,color="green",shape="box"];15830[label="compare vz5040 vz5030",fontsize=16,color="burlywood",shape="box"];16101[label="vz5040/vz50400 :% vz50401",fontsize=10,color="white",style="solid",shape="box"];15830 -> 16101[label="",style="solid", color="burlywood", weight=9];
16101 -> 15859[label="",style="solid", color="burlywood", weight=3];
15831[label="vz5030",fontsize=16,color="green",shape="box"];15832[label="vz5031",fontsize=16,color="green",shape="box"];15833[label="vz5041",fontsize=16,color="green",shape="box"];15828[label="merge0 vz511 compare vz512 vz513 vz514 vz515\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];16102[label="vz515/LT",fontsize=10,color="white",style="solid",shape="box"];15828 -> 16102[label="",style="solid", color="burlywood", weight=9];
16102 -> 15860[label="",style="solid", color="burlywood", weight=3];
16103[label="vz515/EQ",fontsize=10,color="white",style="solid",shape="box"];15828 -> 16103[label="",style="solid", color="burlywood", weight=9];
16103 -> 15861[label="",style="solid", color="burlywood", weight=3];
16104[label="vz515/GT",fontsize=10,color="white",style="solid",shape="box"];15828 -> 16104[label="",style="solid", color="burlywood", weight=9];
16104 -> 15862[label="",style="solid", color="burlywood", weight=3];
15791 -> 15606[label="",style="dashed", color="red", weight=0];
15791[label="mergesort' compare (merge compare vz501 (merge compare vz5020 vz50210) : merge_pairs compare (merge_pairs compare vz50211))\n  Ord a",fontsize=16,color="magenta"];15791 -> 15794[label="",style="dashed", color="magenta", weight=3];
15791 -> 15795[label="",style="dashed", color="magenta", weight=3];
15792 -> 15606[label="",style="dashed", color="red", weight=0];
15792[label="mergesort' compare (merge compare vz501 vz5020 : merge_pairs compare [])\n  Ord a",fontsize=16,color="magenta"];15792 -> 15796[label="",style="dashed", color="magenta", weight=3];
15792 -> 15797[label="",style="dashed", color="magenta", weight=3];
15859[label="compare (vz50400 :% vz50401) vz5030",fontsize=16,color="burlywood",shape="box"];16107[label="vz5030/vz50300 :% vz50301",fontsize=10,color="white",style="solid",shape="box"];15859 -> 16107[label="",style="solid", color="burlywood", weight=9];
16107 -> 15894[label="",style="solid", color="burlywood", weight=3];
15860[label="merge0 vz511 compare vz512 vz513 vz514 LT\n  Ord a",fontsize=16,color="black",shape="box"];15860 -> 15895[label="",style="solid", color="black", weight=3];
15861[label="merge0 vz511 compare vz512 vz513 vz514 EQ\n  Ord a",fontsize=16,color="black",shape="box"];15861 -> 15896[label="",style="solid", color="black", weight=3];
15862[label="merge0 vz511 compare vz512 vz513 vz514 GT\n  Ord a",fontsize=16,color="black",shape="box"];15862 -> 15897[label="",style="solid", color="black", weight=3];
15794[label="merge compare vz501 (merge compare vz5020 vz50210)\n  Ord a",fontsize=16,color="burlywood",shape="box"];16108[label="vz50210/vz502100 : vz502101",fontsize=10,color="white",style="solid",shape="box"];15794 -> 16108[label="",style="solid", color="burlywood", weight=9];
16108 -> 15799[label="",style="solid", color="burlywood", weight=3];
16109[label="vz50210/[]",fontsize=10,color="white",style="solid",shape="box"];15794 -> 16109[label="",style="solid", color="burlywood", weight=9];
16109 -> 15800[label="",style="solid", color="burlywood", weight=3];
15795[label="merge_pairs compare vz50211\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];16110[label="vz50211/vz502110 : vz502111",fontsize=10,color="white",style="solid",shape="box"];15795 -> 16110[label="",style="solid", color="burlywood", weight=9];
16110 -> 15801[label="",style="solid", color="burlywood", weight=3];
16111[label="vz50211/[]",fontsize=10,color="white",style="solid",shape="box"];15795 -> 16111[label="",style="solid", color="burlywood", weight=9];
16111 -> 15802[label="",style="solid", color="burlywood", weight=3];
15796[label="merge compare vz501 vz5020\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];16112[label="vz5020/vz50200 : vz50201",fontsize=10,color="white",style="solid",shape="box"];15796 -> 16112[label="",style="solid", color="burlywood", weight=9];
16112 -> 15803[label="",style="solid", color="burlywood", weight=3];
16113[label="vz5020/[]",fontsize=10,color="white",style="solid",shape="box"];15796 -> 16113[label="",style="solid", color="burlywood", weight=9];
16113 -> 15804[label="",style="solid", color="burlywood", weight=3];
15797[label="[]\n  Ord a",fontsize=16,color="green",shape="box"];15894[label="compare (vz50400 :% vz50401) (vz50300 :% vz50301)",fontsize=16,color="black",shape="box"];15894 -> 15940[label="",style="solid", color="black", weight=3];
15895[label="vz512 : merge compare vz513 (vz511 : vz514)\n  Ord a",fontsize=16,color="green",shape="box"];15895 -> 15941[label="",style="dashed", color="green", weight=3];
15896[label="vz512 : merge compare vz513 (vz511 : vz514)\n  Ord a",fontsize=16,color="green",shape="box"];15896 -> 15942[label="",style="dashed", color="green", weight=3];
15897[label="vz511 : merge compare (vz512 : vz513) vz514\n  Ord a",fontsize=16,color="green",shape="box"];15897 -> 15943[label="",style="dashed", color="green", weight=3];
15799[label="merge compare vz501 (merge compare vz5020 (vz502100 : vz502101))\n  Ord a",fontsize=16,color="burlywood",shape="box"];16114[label="vz5020/vz50200 : vz50201",fontsize=10,color="white",style="solid",shape="box"];15799 -> 16114[label="",style="solid", color="burlywood", weight=9];
16114 -> 15806[label="",style="solid", color="burlywood", weight=3];
16115[label="vz5020/[]",fontsize=10,color="white",style="solid",shape="box"];15799 -> 16115[label="",style="solid", color="burlywood", weight=9];
16115 -> 15807[label="",style="solid", color="burlywood", weight=3];
15800[label="merge compare vz501 (merge compare vz5020 [])\n  Ord a",fontsize=16,color="black",shape="box"];15800 -> 15808[label="",style="solid", color="black", weight=3];
15801[label="merge_pairs compare (vz502110 : vz502111)\n  Ord a",fontsize=16,color="burlywood",shape="box"];16116[label="vz502111/vz5021110 : vz5021111",fontsize=10,color="white",style="solid",shape="box"];15801 -> 16116[label="",style="solid", color="burlywood", weight=9];
16116 -> 15809[label="",style="solid", color="burlywood", weight=3];
16117[label="vz502111/[]",fontsize=10,color="white",style="solid",shape="box"];15801 -> 16117[label="",style="solid", color="burlywood", weight=9];
16117 -> 15810[label="",style="solid", color="burlywood", weight=3];
15802[label="merge_pairs compare []\n  Ord a",fontsize=16,color="black",shape="box"];15802 -> 15811[label="",style="solid", color="black", weight=3];
15803[label="merge compare vz501 (vz50200 : vz50201)\n  Ord a",fontsize=16,color="burlywood",shape="box"];16118[label="vz501/vz5010 : vz5011",fontsize=10,color="white",style="solid",shape="box"];15803 -> 16118[label="",style="solid", color="burlywood", weight=9];
16118 -> 15812[label="",style="solid", color="burlywood", weight=3];
16119[label="vz501/[]",fontsize=10,color="white",style="solid",shape="box"];15803 -> 16119[label="",style="solid", color="burlywood", weight=9];
16119 -> 15813[label="",style="solid", color="burlywood", weight=3];
15804[label="merge compare vz501 []\n  Ord a",fontsize=16,color="black",shape="box"];15804 -> 15814[label="",style="solid", color="black", weight=3];
15940 -> 15876[label="",style="dashed", color="red", weight=0];
15940[label="compare (vz50400 * vz50301) (vz50300 * vz50401)",fontsize=16,color="magenta"];15940 -> 15947[label="",style="dashed", color="magenta", weight=3];
15940 -> 15948[label="",style="dashed", color="magenta", weight=3];
15941 -> 15796[label="",style="dashed", color="red", weight=0];
15941[label="merge compare vz513 (vz511 : vz514)\n  Ord a",fontsize=16,color="magenta"];15941 -> 15949[label="",style="dashed", color="magenta", weight=3];
15941 -> 15950[label="",style="dashed", color="magenta", weight=3];
15942 -> 15796[label="",style="dashed", color="red", weight=0];
15942[label="merge compare vz513 (vz511 : vz514)\n  Ord a",fontsize=16,color="magenta"];15942 -> 15951[label="",style="dashed", color="magenta", weight=3];
15942 -> 15952[label="",style="dashed", color="magenta", weight=3];
15943 -> 15796[label="",style="dashed", color="red", weight=0];
15943[label="merge compare (vz512 : vz513) vz514\n  Ord a",fontsize=16,color="magenta"];15943 -> 15953[label="",style="dashed", color="magenta", weight=3];
15943 -> 15954[label="",style="dashed", color="magenta", weight=3];
15806[label="merge compare vz501 (merge compare (vz50200 : vz50201) (vz502100 : vz502101))\n  Ord a",fontsize=16,color="black",shape="box"];15806 -> 15816[label="",style="solid", color="black", weight=3];
15807[label="merge compare vz501 (merge compare [] (vz502100 : vz502101))\n  Ord a",fontsize=16,color="black",shape="box"];15807 -> 15817[label="",style="solid", color="black", weight=3];
15808 -> 15796[label="",style="dashed", color="red", weight=0];
15808[label="merge compare vz501 vz5020\n  Ord a",fontsize=16,color="magenta"];15809[label="merge_pairs compare (vz502110 : vz5021110 : vz5021111)\n  Ord a",fontsize=16,color="black",shape="box"];15809 -> 15818[label="",style="solid", color="black", weight=3];
15810[label="merge_pairs compare (vz502110 : [])\n  Ord a",fontsize=16,color="black",shape="box"];15810 -> 15819[label="",style="solid", color="black", weight=3];
15811[label="[]\n  Ord a",fontsize=16,color="green",shape="box"];15812[label="merge compare (vz5010 : vz5011) (vz50200 : vz50201)\n  Ord a",fontsize=16,color="black",shape="box"];15812 -> 15820[label="",style="solid", color="black", weight=3];
15813[label="merge compare [] (vz50200 : vz50201)\n  Ord a",fontsize=16,color="black",shape="box"];15813 -> 15821[label="",style="solid", color="black", weight=3];
15814[label="vz501\n  Ord a",fontsize=16,color="green",shape="box"];15947[label="vz50300 * vz50401",fontsize=16,color="black",shape="triangle"];15947 -> 15960[label="",style="solid", color="black", weight=3];
15948 -> 15947[label="",style="dashed", color="red", weight=0];
15948[label="vz50400 * vz50301",fontsize=16,color="magenta"];15948 -> 15961[label="",style="dashed", color="magenta", weight=3];
15948 -> 15962[label="",style="dashed", color="magenta", weight=3];
15876[label="compare vz5010 vz50200",fontsize=16,color="black",shape="triangle"];15876 -> 15908[label="",style="solid", color="black", weight=3];
15949[label="vz511 : vz514\n  Ord a",fontsize=16,color="green",shape="box"];15950[label="vz513\n  Ord a",fontsize=16,color="green",shape="box"];15951[label="vz511 : vz514\n  Ord a",fontsize=16,color="green",shape="box"];15952[label="vz513\n  Ord a",fontsize=16,color="green",shape="box"];15953[label="vz514\n  Ord a",fontsize=16,color="green",shape="box"];15954[label="vz512 : vz513\n  Ord a",fontsize=16,color="green",shape="box"];15816 -> 15796[label="",style="dashed", color="red", weight=0];
15816[label="merge compare vz501 (merge0 vz502100 compare vz50200 vz50201 vz502101 (compare vz50200 vz502100))\n  Ord a",fontsize=16,color="magenta"];15816 -> 15824[label="",style="dashed", color="magenta", weight=3];
15817 -> 15796[label="",style="dashed", color="red", weight=0];
15817[label="merge compare vz501 (vz502100 : vz502101)\n  Ord a",fontsize=16,color="magenta"];15817 -> 15825[label="",style="dashed", color="magenta", weight=3];
15818[label="merge compare vz502110 vz5021110 : merge_pairs compare vz5021111\n  Ord a",fontsize=16,color="green",shape="box"];15818 -> 15826[label="",style="dashed", color="green", weight=3];
15818 -> 15827[label="",style="dashed", color="green", weight=3];
15819[label="vz502110 : []\n  Ord a",fontsize=16,color="green",shape="box"];15820 -> 15828[label="",style="dashed", color="red", weight=0];
15820[label="merge0 vz50200 compare vz5010 vz5011 vz50201 (compare vz5010 vz50200)\n  Ord a",fontsize=16,color="magenta"];15820 -> 15849[label="",style="dashed", color="magenta", weight=3];
15820 -> 15850[label="",style="dashed", color="magenta", weight=3];
15820 -> 15851[label="",style="dashed", color="magenta", weight=3];
15820 -> 15852[label="",style="dashed", color="magenta", weight=3];
15820 -> 15853[label="",style="dashed", color="magenta", weight=3];
15821[label="vz50200 : vz50201\n  Ord a",fontsize=16,color="green",shape="box"];15960[label="primMulInt vz50300 vz50401",fontsize=16,color="burlywood",shape="box"];16129[label="vz50300/Pos vz503000",fontsize=10,color="white",style="solid",shape="box"];15960 -> 16129[label="",style="solid", color="burlywood", weight=9];
16129 -> 15973[label="",style="solid", color="burlywood", weight=3];
16130[label="vz50300/Neg vz503000",fontsize=10,color="white",style="solid",shape="box"];15960 -> 16130[label="",style="solid", color="burlywood", weight=9];
16130 -> 15974[label="",style="solid", color="burlywood", weight=3];
15961[label="vz50301",fontsize=16,color="green",shape="box"];15962[label="vz50400",fontsize=16,color="green",shape="box"];15908[label="primCmpInt vz5010 vz50200",fontsize=16,color="burlywood",shape="box"];16131[label="vz5010/Pos vz50100",fontsize=10,color="white",style="solid",shape="box"];15908 -> 16131[label="",style="solid", color="burlywood", weight=9];
16131 -> 15945[label="",style="solid", color="burlywood", weight=3];
16132[label="vz5010/Neg vz50100",fontsize=10,color="white",style="solid",shape="box"];15908 -> 16132[label="",style="solid", color="burlywood", weight=9];
16132 -> 15946[label="",style="solid", color="burlywood", weight=3];
15824 -> 15828[label="",style="dashed", color="red", weight=0];
15824[label="merge0 vz502100 compare vz50200 vz50201 vz502101 (compare vz50200 vz502100)\n  Ord a",fontsize=16,color="magenta"];15824 -> 15854[label="",style="dashed", color="magenta", weight=3];
15824 -> 15855[label="",style="dashed", color="magenta", weight=3];
15824 -> 15856[label="",style="dashed", color="magenta", weight=3];
15824 -> 15857[label="",style="dashed", color="magenta", weight=3];
15824 -> 15858[label="",style="dashed", color="magenta", weight=3];
15825[label="vz502100 : vz502101\n  Ord a",fontsize=16,color="green",shape="box"];15826 -> 15796[label="",style="dashed", color="red", weight=0];
15826[label="merge compare vz502110 vz5021110\n  Ord a",fontsize=16,color="magenta"];15826 -> 15863[label="",style="dashed", color="magenta", weight=3];
15826 -> 15864[label="",style="dashed", color="magenta", weight=3];
15827 -> 15795[label="",style="dashed", color="red", weight=0];
15827[label="merge_pairs compare vz5021111\n  Ord a",fontsize=16,color="magenta"];15827 -> 15865[label="",style="dashed", color="magenta", weight=3];
15849[label="vz5010\n  Ord a",fontsize=16,color="green",shape="box"];15850[label="compare vz5010 vz50200\n  Ord a",fontsize=16,color="blue",shape="box"];16136[label="compare :: (Maybe a) -> (Maybe a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16136[label="",style="solid", color="blue", weight=9];
16136 -> 15866[label="",style="solid", color="blue", weight=3];
16137[label="compare :: ((@2) a b) -> ((@2) a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16137[label="",style="solid", color="blue", weight=9];
16137 -> 15867[label="",style="solid", color="blue", weight=3];
16138[label="compare :: Float -> Float -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16138[label="",style="solid", color="blue", weight=9];
16138 -> 15868[label="",style="solid", color="blue", weight=3];
16139[label="compare :: () -> () -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16139[label="",style="solid", color="blue", weight=9];
16139 -> 15869[label="",style="solid", color="blue", weight=3];
16140[label="compare :: (Either a b) -> (Either a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16140[label="",style="solid", color="blue", weight=9];
16140 -> 15870[label="",style="solid", color="blue", weight=3];
16141[label="compare :: Char -> Char -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16141[label="",style="solid", color="blue", weight=9];
16141 -> 15871[label="",style="solid", color="blue", weight=3];
16142[label="compare :: (Ratio a) -> (Ratio a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16142[label="",style="solid", color="blue", weight=9];
16142 -> 15872[label="",style="solid", color="blue", weight=3];
16143[label="compare :: Double -> Double -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16143[label="",style="solid", color="blue", weight=9];
16143 -> 15873[label="",style="solid", color="blue", weight=3];
16144[label="compare :: ((@3) a b c) -> ((@3) a b c) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16144[label="",style="solid", color="blue", weight=9];
16144 -> 15874[label="",style="solid", color="blue", weight=3];
16145[label="compare :: ([] a) -> ([] a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16145[label="",style="solid", color="blue", weight=9];
16145 -> 15875[label="",style="solid", color="blue", weight=3];
16146[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16146[label="",style="solid", color="blue", weight=9];
16146 -> 15876[label="",style="solid", color="blue", weight=3];
16147[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16147[label="",style="solid", color="blue", weight=9];
16147 -> 15877[label="",style="solid", color="blue", weight=3];
16148[label="compare :: Ordering -> Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16148[label="",style="solid", color="blue", weight=9];
16148 -> 15878[label="",style="solid", color="blue", weight=3];
16149[label="compare :: Bool -> Bool -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15850 -> 16149[label="",style="solid", color="blue", weight=9];
16149 -> 15879[label="",style="solid", color="blue", weight=3];
15851[label="vz50200\n  Ord a",fontsize=16,color="green",shape="box"];15852[label="vz50201\n  Ord a",fontsize=16,color="green",shape="box"];15853[label="vz5011\n  Ord a",fontsize=16,color="green",shape="box"];15973[label="primMulInt (Pos vz503000) vz50401",fontsize=16,color="burlywood",shape="box"];16150[label="vz50401/Pos vz504010",fontsize=10,color="white",style="solid",shape="box"];15973 -> 16150[label="",style="solid", color="burlywood", weight=9];
16150 -> 15991[label="",style="solid", color="burlywood", weight=3];
16151[label="vz50401/Neg vz504010",fontsize=10,color="white",style="solid",shape="box"];15973 -> 16151[label="",style="solid", color="burlywood", weight=9];
16151 -> 15992[label="",style="solid", color="burlywood", weight=3];
15974[label="primMulInt (Neg vz503000) vz50401",fontsize=16,color="burlywood",shape="box"];16152[label="vz50401/Pos vz504010",fontsize=10,color="white",style="solid",shape="box"];15974 -> 16152[label="",style="solid", color="burlywood", weight=9];
16152 -> 15993[label="",style="solid", color="burlywood", weight=3];
16153[label="vz50401/Neg vz504010",fontsize=10,color="white",style="solid",shape="box"];15974 -> 16153[label="",style="solid", color="burlywood", weight=9];
16153 -> 15994[label="",style="solid", color="burlywood", weight=3];
15945[label="primCmpInt (Pos vz50100) vz50200",fontsize=16,color="burlywood",shape="box"];16154[label="vz50100/Succ vz501000",fontsize=10,color="white",style="solid",shape="box"];15945 -> 16154[label="",style="solid", color="burlywood", weight=9];
16154 -> 15956[label="",style="solid", color="burlywood", weight=3];
16155[label="vz50100/Zero",fontsize=10,color="white",style="solid",shape="box"];15945 -> 16155[label="",style="solid", color="burlywood", weight=9];
16155 -> 15957[label="",style="solid", color="burlywood", weight=3];
15946[label="primCmpInt (Neg vz50100) vz50200",fontsize=16,color="burlywood",shape="box"];16156[label="vz50100/Succ vz501000",fontsize=10,color="white",style="solid",shape="box"];15946 -> 16156[label="",style="solid", color="burlywood", weight=9];
16156 -> 15958[label="",style="solid", color="burlywood", weight=3];
16157[label="vz50100/Zero",fontsize=10,color="white",style="solid",shape="box"];15946 -> 16157[label="",style="solid", color="burlywood", weight=9];
16157 -> 15959[label="",style="solid", color="burlywood", weight=3];
15854[label="vz50200\n  Ord a",fontsize=16,color="green",shape="box"];15855[label="compare vz50200 vz502100\n  Ord a",fontsize=16,color="blue",shape="box"];16158[label="compare :: (Maybe a) -> (Maybe a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16158[label="",style="solid", color="blue", weight=9];
16158 -> 15880[label="",style="solid", color="blue", weight=3];
16159[label="compare :: ((@2) a b) -> ((@2) a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16159[label="",style="solid", color="blue", weight=9];
16159 -> 15881[label="",style="solid", color="blue", weight=3];
16160[label="compare :: Float -> Float -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16160[label="",style="solid", color="blue", weight=9];
16160 -> 15882[label="",style="solid", color="blue", weight=3];
16161[label="compare :: () -> () -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16161[label="",style="solid", color="blue", weight=9];
16161 -> 15883[label="",style="solid", color="blue", weight=3];
16162[label="compare :: (Either a b) -> (Either a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16162[label="",style="solid", color="blue", weight=9];
16162 -> 15884[label="",style="solid", color="blue", weight=3];
16163[label="compare :: Char -> Char -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16163[label="",style="solid", color="blue", weight=9];
16163 -> 15885[label="",style="solid", color="blue", weight=3];
16164[label="compare :: (Ratio a) -> (Ratio a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16164[label="",style="solid", color="blue", weight=9];
16164 -> 15886[label="",style="solid", color="blue", weight=3];
16165[label="compare :: Double -> Double -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16165[label="",style="solid", color="blue", weight=9];
16165 -> 15887[label="",style="solid", color="blue", weight=3];
16166[label="compare :: ((@3) a b c) -> ((@3) a b c) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16166[label="",style="solid", color="blue", weight=9];
16166 -> 15888[label="",style="solid", color="blue", weight=3];
16167[label="compare :: ([] a) -> ([] a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16167[label="",style="solid", color="blue", weight=9];
16167 -> 15889[label="",style="solid", color="blue", weight=3];
16168[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16168[label="",style="solid", color="blue", weight=9];
16168 -> 15890[label="",style="solid", color="blue", weight=3];
16169[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16169[label="",style="solid", color="blue", weight=9];
16169 -> 15891[label="",style="solid", color="blue", weight=3];
16170[label="compare :: Ordering -> Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16170[label="",style="solid", color="blue", weight=9];
16170 -> 15892[label="",style="solid", color="blue", weight=3];
16171[label="compare :: Bool -> Bool -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15855 -> 16171[label="",style="solid", color="blue", weight=9];
16171 -> 15893[label="",style="solid", color="blue", weight=3];
15856[label="vz502100\n  Ord a",fontsize=16,color="green",shape="box"];15857[label="vz502101\n  Ord a",fontsize=16,color="green",shape="box"];15858[label="vz50201\n  Ord a",fontsize=16,color="green",shape="box"];15863[label="vz5021110\n  Ord a",fontsize=16,color="green",shape="box"];15864[label="vz502110\n  Ord a",fontsize=16,color="green",shape="box"];15865[label="vz5021111\n  Ord a",fontsize=16,color="green",shape="box"];15866[label="compare vz5010 vz50200\n  Ord a",fontsize=16,color="black",shape="triangle"];15866 -> 15898[label="",style="solid", color="black", weight=3];
15867[label="compare vz5010 vz50200\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];15867 -> 15899[label="",style="solid", color="black", weight=3];
15868[label="compare vz5010 vz50200",fontsize=16,color="black",shape="triangle"];15868 -> 15900[label="",style="solid", color="black", weight=3];
15869[label="compare vz5010 vz50200",fontsize=16,color="black",shape="triangle"];15869 -> 15901[label="",style="solid", color="black", weight=3];
15870[label="compare vz5010 vz50200\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];15870 -> 15902[label="",style="solid", color="black", weight=3];
15871[label="compare vz5010 vz50200",fontsize=16,color="black",shape="triangle"];15871 -> 15903[label="",style="solid", color="black", weight=3];
15872[label="compare vz5010 vz50200\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];16172[label="vz5010/vz50100 :% vz50101",fontsize=10,color="white",style="solid",shape="box"];15872 -> 16172[label="",style="solid", color="burlywood", weight=9];
16172 -> 15904[label="",style="solid", color="burlywood", weight=3];
15873[label="compare vz5010 vz50200",fontsize=16,color="black",shape="triangle"];15873 -> 15905[label="",style="solid", color="black", weight=3];
15874[label="compare vz5010 vz50200\n  Ord a  Ord b  Ord c",fontsize=16,color="black",shape="triangle"];15874 -> 15906[label="",style="solid", color="black", weight=3];
15875[label="compare vz5010 vz50200\n  Ord a",fontsize=16,color="black",shape="triangle"];15875 -> 15907[label="",style="solid", color="black", weight=3];
15877[label="compare vz5010 vz50200",fontsize=16,color="black",shape="triangle"];15877 -> 15909[label="",style="solid", color="black", weight=3];
15878[label="compare vz5010 vz50200",fontsize=16,color="black",shape="triangle"];15878 -> 15910[label="",style="solid", color="black", weight=3];
15879[label="compare vz5010 vz50200",fontsize=16,color="black",shape="triangle"];15879 -> 15911[label="",style="solid", color="black", weight=3];
15991[label="primMulInt (Pos vz503000) (Pos vz504010)",fontsize=16,color="black",shape="box"];15991 -> 16014[label="",style="solid", color="black", weight=3];
15992[label="primMulInt (Pos vz503000) (Neg vz504010)",fontsize=16,color="black",shape="box"];15992 -> 16015[label="",style="solid", color="black", weight=3];
15993[label="primMulInt (Neg vz503000) (Pos vz504010)",fontsize=16,color="black",shape="box"];15993 -> 16016[label="",style="solid", color="black", weight=3];
15994[label="primMulInt (Neg vz503000) (Neg vz504010)",fontsize=16,color="black",shape="box"];15994 -> 16017[label="",style="solid", color="black", weight=3];
15956[label="primCmpInt (Pos (Succ vz501000)) vz50200",fontsize=16,color="burlywood",shape="box"];16173[label="vz50200/Pos vz502000",fontsize=10,color="white",style="solid",shape="box"];15956 -> 16173[label="",style="solid", color="burlywood", weight=9];
16173 -> 15965[label="",style="solid", color="burlywood", weight=3];
16174[label="vz50200/Neg vz502000",fontsize=10,color="white",style="solid",shape="box"];15956 -> 16174[label="",style="solid", color="burlywood", weight=9];
16174 -> 15966[label="",style="solid", color="burlywood", weight=3];
15957[label="primCmpInt (Pos Zero) vz50200",fontsize=16,color="burlywood",shape="box"];16175[label="vz50200/Pos vz502000",fontsize=10,color="white",style="solid",shape="box"];15957 -> 16175[label="",style="solid", color="burlywood", weight=9];
16175 -> 15967[label="",style="solid", color="burlywood", weight=3];
16176[label="vz50200/Neg vz502000",fontsize=10,color="white",style="solid",shape="box"];15957 -> 16176[label="",style="solid", color="burlywood", weight=9];
16176 -> 15968[label="",style="solid", color="burlywood", weight=3];
15958[label="primCmpInt (Neg (Succ vz501000)) vz50200",fontsize=16,color="burlywood",shape="box"];16177[label="vz50200/Pos vz502000",fontsize=10,color="white",style="solid",shape="box"];15958 -> 16177[label="",style="solid", color="burlywood", weight=9];
16177 -> 15969[label="",style="solid", color="burlywood", weight=3];
16178[label="vz50200/Neg vz502000",fontsize=10,color="white",style="solid",shape="box"];15958 -> 16178[label="",style="solid", color="burlywood", weight=9];
16178 -> 15970[label="",style="solid", color="burlywood", weight=3];
15959[label="primCmpInt (Neg Zero) vz50200",fontsize=16,color="burlywood",shape="box"];16179[label="vz50200/Pos vz502000",fontsize=10,color="white",style="solid",shape="box"];15959 -> 16179[label="",style="solid", color="burlywood", weight=9];
16179 -> 15971[label="",style="solid", color="burlywood", weight=3];
16180[label="vz50200/Neg vz502000",fontsize=10,color="white",style="solid",shape="box"];15959 -> 16180[label="",style="solid", color="burlywood", weight=9];
16180 -> 15972[label="",style="solid", color="burlywood", weight=3];
15880 -> 15866[label="",style="dashed", color="red", weight=0];
15880[label="compare vz50200 vz502100\n  Ord a",fontsize=16,color="magenta"];15880 -> 15912[label="",style="dashed", color="magenta", weight=3];
15880 -> 15913[label="",style="dashed", color="magenta", weight=3];
15881 -> 15867[label="",style="dashed", color="red", weight=0];
15881[label="compare vz50200 vz502100\n  Ord a  Ord b",fontsize=16,color="magenta"];15881 -> 15914[label="",style="dashed", color="magenta", weight=3];
15881 -> 15915[label="",style="dashed", color="magenta", weight=3];
15882 -> 15868[label="",style="dashed", color="red", weight=0];
15882[label="compare vz50200 vz502100",fontsize=16,color="magenta"];15882 -> 15916[label="",style="dashed", color="magenta", weight=3];
15882 -> 15917[label="",style="dashed", color="magenta", weight=3];
15883 -> 15869[label="",style="dashed", color="red", weight=0];
15883[label="compare vz50200 vz502100",fontsize=16,color="magenta"];15883 -> 15918[label="",style="dashed", color="magenta", weight=3];
15883 -> 15919[label="",style="dashed", color="magenta", weight=3];
15884 -> 15870[label="",style="dashed", color="red", weight=0];
15884[label="compare vz50200 vz502100\n  Ord a  Ord b",fontsize=16,color="magenta"];15884 -> 15920[label="",style="dashed", color="magenta", weight=3];
15884 -> 15921[label="",style="dashed", color="magenta", weight=3];
15885 -> 15871[label="",style="dashed", color="red", weight=0];
15885[label="compare vz50200 vz502100",fontsize=16,color="magenta"];15885 -> 15922[label="",style="dashed", color="magenta", weight=3];
15885 -> 15923[label="",style="dashed", color="magenta", weight=3];
15886 -> 15872[label="",style="dashed", color="red", weight=0];
15886[label="compare vz50200 vz502100\n  Integral a",fontsize=16,color="magenta"];15886 -> 15924[label="",style="dashed", color="magenta", weight=3];
15886 -> 15925[label="",style="dashed", color="magenta", weight=3];
15887 -> 15873[label="",style="dashed", color="red", weight=0];
15887[label="compare vz50200 vz502100",fontsize=16,color="magenta"];15887 -> 15926[label="",style="dashed", color="magenta", weight=3];
15887 -> 15927[label="",style="dashed", color="magenta", weight=3];
15888 -> 15874[label="",style="dashed", color="red", weight=0];
15888[label="compare vz50200 vz502100\n  Ord a  Ord b  Ord c",fontsize=16,color="magenta"];15888 -> 15928[label="",style="dashed", color="magenta", weight=3];
15888 -> 15929[label="",style="dashed", color="magenta", weight=3];
15889 -> 15875[label="",style="dashed", color="red", weight=0];
15889[label="compare vz50200 vz502100\n  Ord a",fontsize=16,color="magenta"];15889 -> 15930[label="",style="dashed", color="magenta", weight=3];
15889 -> 15931[label="",style="dashed", color="magenta", weight=3];
15890 -> 15876[label="",style="dashed", color="red", weight=0];
15890[label="compare vz50200 vz502100",fontsize=16,color="magenta"];15890 -> 15932[label="",style="dashed", color="magenta", weight=3];
15890 -> 15933[label="",style="dashed", color="magenta", weight=3];
15891 -> 15877[label="",style="dashed", color="red", weight=0];
15891[label="compare vz50200 vz502100",fontsize=16,color="magenta"];15891 -> 15934[label="",style="dashed", color="magenta", weight=3];
15891 -> 15935[label="",style="dashed", color="magenta", weight=3];
15892 -> 15878[label="",style="dashed", color="red", weight=0];
15892[label="compare vz50200 vz502100",fontsize=16,color="magenta"];15892 -> 15936[label="",style="dashed", color="magenta", weight=3];
15892 -> 15937[label="",style="dashed", color="magenta", weight=3];
15893 -> 15879[label="",style="dashed", color="red", weight=0];
15893[label="compare vz50200 vz502100",fontsize=16,color="magenta"];15893 -> 15938[label="",style="dashed", color="magenta", weight=3];
15893 -> 15939[label="",style="dashed", color="magenta", weight=3];
15898[label="error []",fontsize=16,color="red",shape="box"];15899[label="error []",fontsize=16,color="red",shape="box"];15900[label="error []",fontsize=16,color="red",shape="box"];15901[label="error []",fontsize=16,color="red",shape="box"];15902[label="error []",fontsize=16,color="red",shape="box"];15903[label="error []",fontsize=16,color="red",shape="box"];15904[label="compare (vz50100 :% vz50101) vz50200\n  Integral a",fontsize=16,color="burlywood",shape="box"];16195[label="vz50200/vz502000 :% vz502001",fontsize=10,color="white",style="solid",shape="box"];15904 -> 16195[label="",style="solid", color="burlywood", weight=9];
16195 -> 15944[label="",style="solid", color="burlywood", weight=3];
15905[label="error []",fontsize=16,color="red",shape="box"];15906[label="error []",fontsize=16,color="red",shape="box"];15907[label="error []",fontsize=16,color="red",shape="box"];15909[label="error []",fontsize=16,color="red",shape="box"];15910[label="error []",fontsize=16,color="red",shape="box"];15911[label="error []",fontsize=16,color="red",shape="box"];16014[label="Pos (primMulNat vz503000 vz504010)",fontsize=16,color="green",shape="box"];16014 -> 16026[label="",style="dashed", color="green", weight=3];
16015[label="Neg (primMulNat vz503000 vz504010)",fontsize=16,color="green",shape="box"];16015 -> 16027[label="",style="dashed", color="green", weight=3];
16016[label="Neg (primMulNat vz503000 vz504010)",fontsize=16,color="green",shape="box"];16016 -> 16028[label="",style="dashed", color="green", weight=3];
16017[label="Pos (primMulNat vz503000 vz504010)",fontsize=16,color="green",shape="box"];16017 -> 16029[label="",style="dashed", color="green", weight=3];
15965[label="primCmpInt (Pos (Succ vz501000)) (Pos vz502000)",fontsize=16,color="black",shape="box"];15965 -> 15979[label="",style="solid", color="black", weight=3];
15966[label="primCmpInt (Pos (Succ vz501000)) (Neg vz502000)",fontsize=16,color="black",shape="box"];15966 -> 15980[label="",style="solid", color="black", weight=3];
15967[label="primCmpInt (Pos Zero) (Pos vz502000)",fontsize=16,color="burlywood",shape="box"];16196[label="vz502000/Succ vz5020000",fontsize=10,color="white",style="solid",shape="box"];15967 -> 16196[label="",style="solid", color="burlywood", weight=9];
16196 -> 15981[label="",style="solid", color="burlywood", weight=3];
16197[label="vz502000/Zero",fontsize=10,color="white",style="solid",shape="box"];15967 -> 16197[label="",style="solid", color="burlywood", weight=9];
16197 -> 15982[label="",style="solid", color="burlywood", weight=3];
15968[label="primCmpInt (Pos Zero) (Neg vz502000)",fontsize=16,color="burlywood",shape="box"];16198[label="vz502000/Succ vz5020000",fontsize=10,color="white",style="solid",shape="box"];15968 -> 16198[label="",style="solid", color="burlywood", weight=9];
16198 -> 15983[label="",style="solid", color="burlywood", weight=3];
16199[label="vz502000/Zero",fontsize=10,color="white",style="solid",shape="box"];15968 -> 16199[label="",style="solid", color="burlywood", weight=9];
16199 -> 15984[label="",style="solid", color="burlywood", weight=3];
15969[label="primCmpInt (Neg (Succ vz501000)) (Pos vz502000)",fontsize=16,color="black",shape="box"];15969 -> 15985[label="",style="solid", color="black", weight=3];
15970[label="primCmpInt (Neg (Succ vz501000)) (Neg vz502000)",fontsize=16,color="black",shape="box"];15970 -> 15986[label="",style="solid", color="black", weight=3];
15971[label="primCmpInt (Neg Zero) (Pos vz502000)",fontsize=16,color="burlywood",shape="box"];16200[label="vz502000/Succ vz5020000",fontsize=10,color="white",style="solid",shape="box"];15971 -> 16200[label="",style="solid", color="burlywood", weight=9];
16200 -> 15987[label="",style="solid", color="burlywood", weight=3];
16201[label="vz502000/Zero",fontsize=10,color="white",style="solid",shape="box"];15971 -> 16201[label="",style="solid", color="burlywood", weight=9];
16201 -> 15988[label="",style="solid", color="burlywood", weight=3];
15972[label="primCmpInt (Neg Zero) (Neg vz502000)",fontsize=16,color="burlywood",shape="box"];16202[label="vz502000/Succ vz5020000",fontsize=10,color="white",style="solid",shape="box"];15972 -> 16202[label="",style="solid", color="burlywood", weight=9];
16202 -> 15989[label="",style="solid", color="burlywood", weight=3];
16203[label="vz502000/Zero",fontsize=10,color="white",style="solid",shape="box"];15972 -> 16203[label="",style="solid", color="burlywood", weight=9];
16203 -> 15990[label="",style="solid", color="burlywood", weight=3];
15912[label="vz502100\n  Ord a",fontsize=16,color="green",shape="box"];15913[label="vz50200\n  Ord a",fontsize=16,color="green",shape="box"];15914[label="vz502100\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];15915[label="vz50200\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];15916[label="vz502100",fontsize=16,color="green",shape="box"];15917[label="vz50200",fontsize=16,color="green",shape="box"];15918[label="vz502100",fontsize=16,color="green",shape="box"];15919[label="vz50200",fontsize=16,color="green",shape="box"];15920[label="vz502100\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];15921[label="vz50200\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];15922[label="vz502100",fontsize=16,color="green",shape="box"];15923[label="vz50200",fontsize=16,color="green",shape="box"];15924[label="vz502100\n  Integral a",fontsize=16,color="green",shape="box"];15925[label="vz50200\n  Integral a",fontsize=16,color="green",shape="box"];15926[label="vz502100",fontsize=16,color="green",shape="box"];15927[label="vz50200",fontsize=16,color="green",shape="box"];15928[label="vz502100\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];15929[label="vz50200\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];15930[label="vz502100\n  Ord a",fontsize=16,color="green",shape="box"];15931[label="vz50200\n  Ord a",fontsize=16,color="green",shape="box"];15932[label="vz502100",fontsize=16,color="green",shape="box"];15933[label="vz50200",fontsize=16,color="green",shape="box"];15934[label="vz502100",fontsize=16,color="green",shape="box"];15935[label="vz50200",fontsize=16,color="green",shape="box"];15936[label="vz502100",fontsize=16,color="green",shape="box"];15937[label="vz50200",fontsize=16,color="green",shape="box"];15938[label="vz502100",fontsize=16,color="green",shape="box"];15939[label="vz50200",fontsize=16,color="green",shape="box"];15944[label="compare (vz50100 :% vz50101) (vz502000 :% vz502001)\n  Integral a",fontsize=16,color="black",shape="box"];15944 -> 15955[label="",style="solid", color="black", weight=3];
16026[label="primMulNat vz503000 vz504010",fontsize=16,color="burlywood",shape="triangle"];16204[label="vz503000/Succ vz5030000",fontsize=10,color="white",style="solid",shape="box"];16026 -> 16204[label="",style="solid", color="burlywood", weight=9];
16204 -> 16034[label="",style="solid", color="burlywood", weight=3];
16205[label="vz503000/Zero",fontsize=10,color="white",style="solid",shape="box"];16026 -> 16205[label="",style="solid", color="burlywood", weight=9];
16205 -> 16035[label="",style="solid", color="burlywood", weight=3];
16027 -> 16026[label="",style="dashed", color="red", weight=0];
16027[label="primMulNat vz503000 vz504010",fontsize=16,color="magenta"];16027 -> 16036[label="",style="dashed", color="magenta", weight=3];
16028 -> 16026[label="",style="dashed", color="red", weight=0];
16028[label="primMulNat vz503000 vz504010",fontsize=16,color="magenta"];16028 -> 16037[label="",style="dashed", color="magenta", weight=3];
16029 -> 16026[label="",style="dashed", color="red", weight=0];
16029[label="primMulNat vz503000 vz504010",fontsize=16,color="magenta"];16029 -> 16038[label="",style="dashed", color="magenta", weight=3];
16029 -> 16039[label="",style="dashed", color="magenta", weight=3];
15979[label="primCmpNat (Succ vz501000) vz502000",fontsize=16,color="burlywood",shape="triangle"];16209[label="vz502000/Succ vz5020000",fontsize=10,color="white",style="solid",shape="box"];15979 -> 16209[label="",style="solid", color="burlywood", weight=9];
16209 -> 16002[label="",style="solid", color="burlywood", weight=3];
16210[label="vz502000/Zero",fontsize=10,color="white",style="solid",shape="box"];15979 -> 16210[label="",style="solid", color="burlywood", weight=9];
16210 -> 16003[label="",style="solid", color="burlywood", weight=3];
15980[label="GT",fontsize=16,color="green",shape="box"];15981[label="primCmpInt (Pos Zero) (Pos (Succ vz5020000))",fontsize=16,color="black",shape="box"];15981 -> 16004[label="",style="solid", color="black", weight=3];
15982[label="primCmpInt (Pos Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];15982 -> 16005[label="",style="solid", color="black", weight=3];
15983[label="primCmpInt (Pos Zero) (Neg (Succ vz5020000))",fontsize=16,color="black",shape="box"];15983 -> 16006[label="",style="solid", color="black", weight=3];
15984[label="primCmpInt (Pos Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];15984 -> 16007[label="",style="solid", color="black", weight=3];
15985[label="LT",fontsize=16,color="green",shape="box"];15986[label="primCmpNat vz502000 (Succ vz501000)",fontsize=16,color="burlywood",shape="triangle"];16211[label="vz502000/Succ vz5020000",fontsize=10,color="white",style="solid",shape="box"];15986 -> 16211[label="",style="solid", color="burlywood", weight=9];
16211 -> 16008[label="",style="solid", color="burlywood", weight=3];
16212[label="vz502000/Zero",fontsize=10,color="white",style="solid",shape="box"];15986 -> 16212[label="",style="solid", color="burlywood", weight=9];
16212 -> 16009[label="",style="solid", color="burlywood", weight=3];
15987[label="primCmpInt (Neg Zero) (Pos (Succ vz5020000))",fontsize=16,color="black",shape="box"];15987 -> 16010[label="",style="solid", color="black", weight=3];
15988[label="primCmpInt (Neg Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];15988 -> 16011[label="",style="solid", color="black", weight=3];
15989[label="primCmpInt (Neg Zero) (Neg (Succ vz5020000))",fontsize=16,color="black",shape="box"];15989 -> 16012[label="",style="solid", color="black", weight=3];
15990[label="primCmpInt (Neg Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];15990 -> 16013[label="",style="solid", color="black", weight=3];
15955[label="compare (vz50100 * vz502001) (vz502000 * vz50101)\n  Integral a",fontsize=16,color="blue",shape="box"];16213[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15955 -> 16213[label="",style="solid", color="blue", weight=9];
16213 -> 15963[label="",style="solid", color="blue", weight=3];
16214[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];15955 -> 16214[label="",style="solid", color="blue", weight=9];
16214 -> 15964[label="",style="solid", color="blue", weight=3];
16034[label="primMulNat (Succ vz5030000) vz504010",fontsize=16,color="burlywood",shape="box"];16215[label="vz504010/Succ vz5040100",fontsize=10,color="white",style="solid",shape="box"];16034 -> 16215[label="",style="solid", color="burlywood", weight=9];
16215 -> 16044[label="",style="solid", color="burlywood", weight=3];
16216[label="vz504010/Zero",fontsize=10,color="white",style="solid",shape="box"];16034 -> 16216[label="",style="solid", color="burlywood", weight=9];
16216 -> 16045[label="",style="solid", color="burlywood", weight=3];
16035[label="primMulNat Zero vz504010",fontsize=16,color="burlywood",shape="box"];16217[label="vz504010/Succ vz5040100",fontsize=10,color="white",style="solid",shape="box"];16035 -> 16217[label="",style="solid", color="burlywood", weight=9];
16217 -> 16046[label="",style="solid", color="burlywood", weight=3];
16218[label="vz504010/Zero",fontsize=10,color="white",style="solid",shape="box"];16035 -> 16218[label="",style="solid", color="burlywood", weight=9];
16218 -> 16047[label="",style="solid", color="burlywood", weight=3];
16036[label="vz504010",fontsize=16,color="green",shape="box"];16037[label="vz503000",fontsize=16,color="green",shape="box"];16038[label="vz503000",fontsize=16,color="green",shape="box"];16039[label="vz504010",fontsize=16,color="green",shape="box"];16002[label="primCmpNat (Succ vz501000) (Succ vz5020000)",fontsize=16,color="black",shape="box"];16002 -> 16018[label="",style="solid", color="black", weight=3];
16003[label="primCmpNat (Succ vz501000) Zero",fontsize=16,color="black",shape="box"];16003 -> 16019[label="",style="solid", color="black", weight=3];
16004 -> 15986[label="",style="dashed", color="red", weight=0];
16004[label="primCmpNat Zero (Succ vz5020000)",fontsize=16,color="magenta"];16004 -> 16020[label="",style="dashed", color="magenta", weight=3];
16004 -> 16021[label="",style="dashed", color="magenta", weight=3];
16005[label="EQ",fontsize=16,color="green",shape="box"];16006[label="GT",fontsize=16,color="green",shape="box"];16007[label="EQ",fontsize=16,color="green",shape="box"];16008[label="primCmpNat (Succ vz5020000) (Succ vz501000)",fontsize=16,color="black",shape="box"];16008 -> 16022[label="",style="solid", color="black", weight=3];
16009[label="primCmpNat Zero (Succ vz501000)",fontsize=16,color="black",shape="box"];16009 -> 16023[label="",style="solid", color="black", weight=3];
16010[label="LT",fontsize=16,color="green",shape="box"];16011[label="EQ",fontsize=16,color="green",shape="box"];16012 -> 15979[label="",style="dashed", color="red", weight=0];
16012[label="primCmpNat (Succ vz5020000) Zero",fontsize=16,color="magenta"];16012 -> 16024[label="",style="dashed", color="magenta", weight=3];
16012 -> 16025[label="",style="dashed", color="magenta", weight=3];
16013[label="EQ",fontsize=16,color="green",shape="box"];15963 -> 15876[label="",style="dashed", color="red", weight=0];
15963[label="compare (vz50100 * vz502001) (vz502000 * vz50101)",fontsize=16,color="magenta"];15963 -> 15975[label="",style="dashed", color="magenta", weight=3];
15963 -> 15976[label="",style="dashed", color="magenta", weight=3];
15964 -> 15877[label="",style="dashed", color="red", weight=0];
15964[label="compare (vz50100 * vz502001) (vz502000 * vz50101)",fontsize=16,color="magenta"];15964 -> 15977[label="",style="dashed", color="magenta", weight=3];
15964 -> 15978[label="",style="dashed", color="magenta", weight=3];
16044[label="primMulNat (Succ vz5030000) (Succ vz5040100)",fontsize=16,color="black",shape="box"];16044 -> 16052[label="",style="solid", color="black", weight=3];
16045[label="primMulNat (Succ vz5030000) Zero",fontsize=16,color="black",shape="box"];16045 -> 16053[label="",style="solid", color="black", weight=3];
16046[label="primMulNat Zero (Succ vz5040100)",fontsize=16,color="black",shape="box"];16046 -> 16054[label="",style="solid", color="black", weight=3];
16047[label="primMulNat Zero Zero",fontsize=16,color="black",shape="box"];16047 -> 16055[label="",style="solid", color="black", weight=3];
16018[label="primCmpNat vz501000 vz5020000",fontsize=16,color="burlywood",shape="triangle"];16223[label="vz501000/Succ vz5010000",fontsize=10,color="white",style="solid",shape="box"];16018 -> 16223[label="",style="solid", color="burlywood", weight=9];
16223 -> 16030[label="",style="solid", color="burlywood", weight=3];
16224[label="vz501000/Zero",fontsize=10,color="white",style="solid",shape="box"];16018 -> 16224[label="",style="solid", color="burlywood", weight=9];
16224 -> 16031[label="",style="solid", color="burlywood", weight=3];
16019[label="GT",fontsize=16,color="green",shape="box"];16020[label="vz5020000",fontsize=16,color="green",shape="box"];16021[label="Zero",fontsize=16,color="green",shape="box"];16022 -> 16018[label="",style="dashed", color="red", weight=0];
16022[label="primCmpNat vz5020000 vz501000",fontsize=16,color="magenta"];16022 -> 16032[label="",style="dashed", color="magenta", weight=3];
16022 -> 16033[label="",style="dashed", color="magenta", weight=3];
16023[label="LT",fontsize=16,color="green",shape="box"];16024[label="Zero",fontsize=16,color="green",shape="box"];16025[label="vz5020000",fontsize=16,color="green",shape="box"];15975 -> 15947[label="",style="dashed", color="red", weight=0];
15975[label="vz502000 * vz50101",fontsize=16,color="magenta"];15975 -> 15995[label="",style="dashed", color="magenta", weight=3];
15975 -> 15996[label="",style="dashed", color="magenta", weight=3];
15976 -> 15947[label="",style="dashed", color="red", weight=0];
15976[label="vz50100 * vz502001",fontsize=16,color="magenta"];15976 -> 15997[label="",style="dashed", color="magenta", weight=3];
15976 -> 15998[label="",style="dashed", color="magenta", weight=3];
15977[label="vz502000 * vz50101",fontsize=16,color="black",shape="triangle"];15977 -> 15999[label="",style="solid", color="black", weight=3];
15978 -> 15977[label="",style="dashed", color="red", weight=0];
15978[label="vz50100 * vz502001",fontsize=16,color="magenta"];15978 -> 16000[label="",style="dashed", color="magenta", weight=3];
15978 -> 16001[label="",style="dashed", color="magenta", weight=3];
16052 -> 16058[label="",style="dashed", color="red", weight=0];
16052[label="primPlusNat (primMulNat vz5030000 (Succ vz5040100)) (Succ vz5040100)",fontsize=16,color="magenta"];16052 -> 16059[label="",style="dashed", color="magenta", weight=3];
16053[label="Zero",fontsize=16,color="green",shape="box"];16054[label="Zero",fontsize=16,color="green",shape="box"];16055[label="Zero",fontsize=16,color="green",shape="box"];16030[label="primCmpNat (Succ vz5010000) vz5020000",fontsize=16,color="burlywood",shape="box"];16230[label="vz5020000/Succ vz50200000",fontsize=10,color="white",style="solid",shape="box"];16030 -> 16230[label="",style="solid", color="burlywood", weight=9];
16230 -> 16040[label="",style="solid", color="burlywood", weight=3];
16231[label="vz5020000/Zero",fontsize=10,color="white",style="solid",shape="box"];16030 -> 16231[label="",style="solid", color="burlywood", weight=9];
16231 -> 16041[label="",style="solid", color="burlywood", weight=3];
16031[label="primCmpNat Zero vz5020000",fontsize=16,color="burlywood",shape="box"];16232[label="vz5020000/Succ vz50200000",fontsize=10,color="white",style="solid",shape="box"];16031 -> 16232[label="",style="solid", color="burlywood", weight=9];
16232 -> 16042[label="",style="solid", color="burlywood", weight=3];
16233[label="vz5020000/Zero",fontsize=10,color="white",style="solid",shape="box"];16031 -> 16233[label="",style="solid", color="burlywood", weight=9];
16233 -> 16043[label="",style="solid", color="burlywood", weight=3];
16032[label="vz501000",fontsize=16,color="green",shape="box"];16033[label="vz5020000",fontsize=16,color="green",shape="box"];15995[label="vz50101",fontsize=16,color="green",shape="box"];15996[label="vz502000",fontsize=16,color="green",shape="box"];15997[label="vz502001",fontsize=16,color="green",shape="box"];15998[label="vz50100",fontsize=16,color="green",shape="box"];15999[label="error []",fontsize=16,color="red",shape="box"];16000[label="vz502001",fontsize=16,color="green",shape="box"];16001[label="vz50100",fontsize=16,color="green",shape="box"];16059 -> 16026[label="",style="dashed", color="red", weight=0];
16059[label="primMulNat vz5030000 (Succ vz5040100)",fontsize=16,color="magenta"];16059 -> 16060[label="",style="dashed", color="magenta", weight=3];
16059 -> 16061[label="",style="dashed", color="magenta", weight=3];
16058[label="primPlusNat vz516 (Succ vz5040100)",fontsize=16,color="burlywood",shape="triangle"];16235[label="vz516/Succ vz5160",fontsize=10,color="white",style="solid",shape="box"];16058 -> 16235[label="",style="solid", color="burlywood", weight=9];
16235 -> 16062[label="",style="solid", color="burlywood", weight=3];
16236[label="vz516/Zero",fontsize=10,color="white",style="solid",shape="box"];16058 -> 16236[label="",style="solid", color="burlywood", weight=9];
16236 -> 16063[label="",style="solid", color="burlywood", weight=3];
16040[label="primCmpNat (Succ vz5010000) (Succ vz50200000)",fontsize=16,color="black",shape="box"];16040 -> 16048[label="",style="solid", color="black", weight=3];
16041[label="primCmpNat (Succ vz5010000) Zero",fontsize=16,color="black",shape="box"];16041 -> 16049[label="",style="solid", color="black", weight=3];
16042[label="primCmpNat Zero (Succ vz50200000)",fontsize=16,color="black",shape="box"];16042 -> 16050[label="",style="solid", color="black", weight=3];
16043[label="primCmpNat Zero Zero",fontsize=16,color="black",shape="box"];16043 -> 16051[label="",style="solid", color="black", weight=3];
16060[label="vz5030000",fontsize=16,color="green",shape="box"];16061[label="Succ vz5040100",fontsize=16,color="green",shape="box"];16062[label="primPlusNat (Succ vz5160) (Succ vz5040100)",fontsize=16,color="black",shape="box"];16062 -> 16064[label="",style="solid", color="black", weight=3];
16063[label="primPlusNat Zero (Succ vz5040100)",fontsize=16,color="black",shape="box"];16063 -> 16065[label="",style="solid", color="black", weight=3];
16048 -> 16018[label="",style="dashed", color="red", weight=0];
16048[label="primCmpNat vz5010000 vz50200000",fontsize=16,color="magenta"];16048 -> 16056[label="",style="dashed", color="magenta", weight=3];
16048 -> 16057[label="",style="dashed", color="magenta", weight=3];
16049[label="GT",fontsize=16,color="green",shape="box"];16050[label="LT",fontsize=16,color="green",shape="box"];16051[label="EQ",fontsize=16,color="green",shape="box"];16064[label="Succ (Succ (primPlusNat vz5160 vz5040100))",fontsize=16,color="green",shape="box"];16064 -> 16066[label="",style="dashed", color="green", weight=3];
16065[label="Succ vz5040100",fontsize=16,color="green",shape="box"];16056[label="vz50200000",fontsize=16,color="green",shape="box"];16057[label="vz5010000",fontsize=16,color="green",shape="box"];16066[label="primPlusNat vz5160 vz5040100",fontsize=16,color="burlywood",shape="triangle"];16238[label="vz5160/Succ vz51600",fontsize=10,color="white",style="solid",shape="box"];16066 -> 16238[label="",style="solid", color="burlywood", weight=9];
16238 -> 16067[label="",style="solid", color="burlywood", weight=3];
16239[label="vz5160/Zero",fontsize=10,color="white",style="solid",shape="box"];16066 -> 16239[label="",style="solid", color="burlywood", weight=9];
16239 -> 16068[label="",style="solid", color="burlywood", weight=3];
16067[label="primPlusNat (Succ vz51600) vz5040100",fontsize=16,color="burlywood",shape="box"];16240[label="vz5040100/Succ vz50401000",fontsize=10,color="white",style="solid",shape="box"];16067 -> 16240[label="",style="solid", color="burlywood", weight=9];
16240 -> 16069[label="",style="solid", color="burlywood", weight=3];
16241[label="vz5040100/Zero",fontsize=10,color="white",style="solid",shape="box"];16067 -> 16241[label="",style="solid", color="burlywood", weight=9];
16241 -> 16070[label="",style="solid", color="burlywood", weight=3];
16068[label="primPlusNat Zero vz5040100",fontsize=16,color="burlywood",shape="box"];16242[label="vz5040100/Succ vz50401000",fontsize=10,color="white",style="solid",shape="box"];16068 -> 16242[label="",style="solid", color="burlywood", weight=9];
16242 -> 16071[label="",style="solid", color="burlywood", weight=3];
16243[label="vz5040100/Zero",fontsize=10,color="white",style="solid",shape="box"];16068 -> 16243[label="",style="solid", color="burlywood", weight=9];
16243 -> 16072[label="",style="solid", color="burlywood", weight=3];
16069[label="primPlusNat (Succ vz51600) (Succ vz50401000)",fontsize=16,color="black",shape="box"];16069 -> 16073[label="",style="solid", color="black", weight=3];
16070[label="primPlusNat (Succ vz51600) Zero",fontsize=16,color="black",shape="box"];16070 -> 16074[label="",style="solid", color="black", weight=3];
16071[label="primPlusNat Zero (Succ vz50401000)",fontsize=16,color="black",shape="box"];16071 -> 16075[label="",style="solid", color="black", weight=3];
16072[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];16072 -> 16076[label="",style="solid", color="black", weight=3];
16073[label="Succ (Succ (primPlusNat vz51600 vz50401000))",fontsize=16,color="green",shape="box"];16073 -> 16077[label="",style="dashed", color="green", weight=3];
16074[label="Succ vz51600",fontsize=16,color="green",shape="box"];16075[label="Succ vz50401000",fontsize=16,color="green",shape="box"];16076[label="Zero",fontsize=16,color="green",shape="box"];16077 -> 16066[label="",style="dashed", color="red", weight=0];
16077[label="primPlusNat vz51600 vz50401000",fontsize=16,color="magenta"];16077 -> 16078[label="",style="dashed", color="magenta", weight=3];
16077 -> 16079[label="",style="dashed", color="magenta", weight=3];
16078[label="vz51600",fontsize=16,color="green",shape="box"];16079[label="vz50401000",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_map(:(vz3110, vz3111)) → new_map(vz3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_map(:(vz3110, vz3111)) → new_map(vz3111)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vz51600), Succ(vz50401000)) → new_primPlusNat(vz51600, vz50401000)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(vz51600), Succ(vz50401000)) → new_primPlusNat(vz51600, vz50401000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vz5030000), Succ(vz5040100)) → new_primMulNat(vz5030000, Succ(vz5040100))

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(vz5030000), Succ(vz5040100)) → new_primMulNat(vz5030000, Succ(vz5040100))
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(vz5010000), Succ(vz50200000)) → new_primCmpNat(vz5010000, vz50200000)

From the DPs we obtained the following set of size-change graphs:

new_primCmpNat(Succ(vz5010000), Succ(vz50200000)) → new_primCmpNat(vz5010000, vz50200000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz511, vz512, vz513, vz514, GT, ba) → new_merge(:(vz512, vz513), vz514, ba)
new_merge0(vz511, vz512, vz513, vz514, EQ, ba) → new_merge(vz513, :(vz511, vz514), ba)
new_merge(:(vz5010, vz5011), :(vz50200, vz50201), bb) → new_merge0(vz50200, vz5010, vz5011, vz50201, new_compare(vz5010, vz50200, bb), bb)
new_merge0(vz511, vz512, vz513, vz514, LT, ba) → new_merge(vz513, :(vz511, vz514), ba)

The TRS R consists of the following rules:

new_sr(Neg(vz503000), Neg(vz504010)) → Pos(new_primMulNat0(vz503000, vz504010))
new_compare(vz5010, vz50200, app(ty_Ratio, ca)) → new_compare2(vz5010, vz50200, ca)
new_primCmpNat1(Succ(vz5010000), Succ(vz50200000)) → new_primCmpNat1(vz5010000, vz50200000)
new_compare3(Neg(Zero), Pos(Zero)) → EQ
new_compare3(Pos(Zero), Neg(Zero)) → EQ
new_compare10(vz5010, vz50200) → error([])
new_compare2(:%(vz50100, vz50101), :%(vz502000, vz502001), ty_Integer) → new_compare4(new_sr0(vz50100, vz502001), new_sr0(vz502000, vz50101))
new_primCmpNat2(Zero, vz501000) → LT
new_sr(Pos(vz503000), Pos(vz504010)) → Pos(new_primMulNat0(vz503000, vz504010))
new_compare(vz5010, vz50200, ty_Char) → new_compare1(vz5010, vz50200)
new_compare(vz5010, vz50200, ty_Bool) → new_compare6(vz5010, vz50200)
new_compare3(Neg(Zero), Pos(Succ(vz5020000))) → LT
new_primPlusNat1(Succ(vz51600), Succ(vz50401000)) → Succ(Succ(new_primPlusNat1(vz51600, vz50401000)))
new_sr0(vz502000, vz50101) → error([])
new_compare(vz5010, vz50200, ty_Float) → new_compare9(vz5010, vz50200)
new_primMulNat0(Zero, Succ(vz5040100)) → Zero
new_primMulNat0(Succ(vz5030000), Zero) → Zero
new_compare(vz5010, vz50200, ty_Int) → new_compare3(vz5010, vz50200)
new_primPlusNat1(Zero, Zero) → Zero
new_compare7(vz5010, vz50200, be) → error([])
new_primCmpNat1(Zero, Succ(vz50200000)) → LT
new_compare8(vz5010, vz50200, bf, bg) → error([])
new_primCmpNat2(Succ(vz5020000), vz501000) → new_primCmpNat1(vz5020000, vz501000)
new_compare(vz5010, vz50200, ty_Double) → new_compare12(vz5010, vz50200)
new_compare(vz5010, vz50200, app(app(app(ty_@3, cb), cc), cd)) → new_compare13(vz5010, vz50200, cb, cc, cd)
new_primMulNat0(Succ(vz5030000), Succ(vz5040100)) → new_primPlusNat0(new_primMulNat0(vz5030000, Succ(vz5040100)), vz5040100)
new_compare2(:%(vz50100, vz50101), :%(vz502000, vz502001), ty_Int) → new_compare3(new_sr(vz50100, vz502001), new_sr(vz502000, vz50101))
new_compare(vz5010, vz50200, app(app(ty_Either, bc), bd)) → new_compare0(vz5010, vz50200, bc, bd)
new_compare9(vz5010, vz50200) → error([])
new_compare(vz5010, vz50200, app(app(ty_@2, bf), bg)) → new_compare8(vz5010, vz50200, bf, bg)
new_compare0(vz5010, vz50200, bc, bd) → error([])
new_compare3(Pos(Zero), Pos(Succ(vz5020000))) → new_primCmpNat2(Zero, vz5020000)
new_compare3(Neg(Succ(vz501000)), Pos(vz502000)) → LT
new_primCmpNat1(Zero, Zero) → EQ
new_compare3(Pos(Zero), Pos(Zero)) → EQ
new_compare3(Pos(Succ(vz501000)), Pos(vz502000)) → new_primCmpNat0(vz501000, vz502000)
new_primCmpNat0(vz501000, Zero) → GT
new_primMulNat0(Zero, Zero) → Zero
new_compare4(vz5010, vz50200) → error([])
new_primPlusNat0(Succ(vz5160), vz5040100) → Succ(Succ(new_primPlusNat1(vz5160, vz5040100)))
new_compare11(vz5010, vz50200, bh) → error([])
new_compare(vz5010, vz50200, ty_Integer) → new_compare4(vz5010, vz50200)
new_compare(vz5010, vz50200, ty_@0) → new_compare5(vz5010, vz50200)
new_compare3(Neg(Succ(vz501000)), Neg(vz502000)) → new_primCmpNat2(vz502000, vz501000)
new_primPlusNat0(Zero, vz5040100) → Succ(vz5040100)
new_primCmpNat1(Succ(vz5010000), Zero) → GT
new_compare3(Neg(Zero), Neg(Succ(vz5020000))) → new_primCmpNat0(vz5020000, Zero)
new_compare1(vz5010, vz50200) → error([])
new_compare6(vz5010, vz50200) → error([])
new_compare5(vz5010, vz50200) → error([])
new_compare12(vz5010, vz50200) → error([])
new_compare(vz5010, vz50200, app(ty_Maybe, be)) → new_compare7(vz5010, vz50200, be)
new_primPlusNat1(Succ(vz51600), Zero) → Succ(vz51600)
new_primPlusNat1(Zero, Succ(vz50401000)) → Succ(vz50401000)
new_compare3(Pos(Zero), Neg(Succ(vz5020000))) → GT
new_sr(Pos(vz503000), Neg(vz504010)) → Neg(new_primMulNat0(vz503000, vz504010))
new_sr(Neg(vz503000), Pos(vz504010)) → Neg(new_primMulNat0(vz503000, vz504010))
new_compare(vz5010, vz50200, ty_Ordering) → new_compare10(vz5010, vz50200)
new_compare3(Neg(Zero), Neg(Zero)) → EQ
new_compare3(Pos(Succ(vz501000)), Neg(vz502000)) → GT
new_primCmpNat0(vz501000, Succ(vz5020000)) → new_primCmpNat1(vz501000, vz5020000)
new_compare13(vz5010, vz50200, cb, cc, cd) → error([])
new_compare(vz5010, vz50200, app(ty_[], bh)) → new_compare11(vz5010, vz50200, bh)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), x1)
new_primCmpNat0(x0, Succ(x1))
new_compare(x0, x1, ty_Bool)
new_compare0(x0, x1, x2, x3)
new_compare9(x0, x1)
new_compare(x0, x1, ty_Integer)
new_primMulNat0(Zero, Zero)
new_compare11(x0, x1, x2)
new_compare(x0, x1, ty_Char)
new_sr0(x0, x1)
new_compare12(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_compare1(x0, x1)
new_compare(x0, x1, ty_Float)
new_compare3(Pos(Succ(x0)), Pos(x1))
new_compare(x0, x1, ty_Ordering)
new_compare5(x0, x1)
new_compare10(x0, x1)
new_compare3(Neg(Zero), Neg(Succ(x0)))
new_primPlusNat1(Zero, Zero)
new_compare2(:%(x0, x1), :%(x2, x3), ty_Integer)
new_primCmpNat1(Zero, Zero)
new_primCmpNat1(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Succ(x0))
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), Zero)
new_compare(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_primCmpNat2(Zero, x0)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare3(Pos(Zero), Pos(Succ(x0)))
new_compare3(Neg(Zero), Neg(Zero))
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare13(x0, x1, x2, x3, x4)
new_compare2(:%(x0, x1), :%(x2, x3), ty_Int)
new_primMulNat0(Succ(x0), Zero)
new_primCmpNat0(x0, Zero)
new_compare(x0, x1, app(ty_[], x2))
new_compare4(x0, x1)
new_sr(Pos(x0), Pos(x1))
new_compare3(Pos(Zero), Neg(Succ(x0)))
new_compare7(x0, x1, x2)
new_compare3(Neg(Zero), Pos(Succ(x0)))
new_compare3(Pos(Zero), Pos(Zero))
new_primCmpNat1(Succ(x0), Zero)
new_compare6(x0, x1)
new_compare3(Neg(Succ(x0)), Neg(x1))
new_primCmpNat2(Succ(x0), x1)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare8(x0, x1, x2, x3)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_sr(Neg(x0), Neg(x1))
new_compare3(Pos(Succ(x0)), Neg(x1))
new_compare3(Neg(Succ(x0)), Pos(x1))
new_primCmpNat1(Zero, Succ(x0))
new_compare3(Pos(Zero), Neg(Zero))
new_compare3(Neg(Zero), Pos(Zero))
new_primPlusNat1(Succ(x0), Succ(x1))
new_compare(x0, x1, ty_@0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_merge0(vz511, vz512, vz513, vz514, EQ, ba) → new_merge(vz513, :(vz511, vz514), ba)
new_merge0(vz511, vz512, vz513, vz514, LT, ba) → new_merge(vz513, :(vz511, vz514), ba)

The remaining pairs can at least be oriented weakly.

new_merge0(vz511, vz512, vz513, vz514, GT, ba) → new_merge(:(vz512, vz513), vz514, ba)
new_merge(:(vz5010, vz5011), :(vz50200, vz50201), bb) → new_merge0(vz50200, vz5010, vz5011, vz50201, new_compare(vz5010, vz50200, bb), bb)

Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₂
POL(:%(x₁, x₂)) = 0
POL(EQ) = 0
POL(GT) = 0
POL(LT) = 0
POL(Neg(x₁)) = 0
POL(Pos(x₁)) = x₁
POL(Succ(x₁)) = 1
POL(Zero) = 1
POL([]) = 0
POL(app(x₁, x₂)) = 0
POL(error(x₁)) = 0
POL(new_compare(x₁, x₂, x₃)) = 0
POL(new_compare0(x₁, x₂, x₃, x₄)) = 0
POL(new_compare1(x₁, x₂)) = 0
POL(new_compare10(x₁, x₂)) = 0
POL(new_compare11(x₁, x₂, x₃)) = 0
POL(new_compare12(x₁, x₂)) = 0
POL(new_compare13(x₁, x₂, x₃, x₄, x₅)) = 0
POL(new_compare2(x₁, x₂, x₃)) = 0
POL(new_compare3(x₁, x₂)) = 0
POL(new_compare4(x₁, x₂)) = 0
POL(new_compare5(x₁, x₂)) = 0
POL(new_compare6(x₁, x₂)) = 0
POL(new_compare7(x₁, x₂, x₃)) = 0
POL(new_compare8(x₁, x₂, x₃, x₄)) = 0
POL(new_compare9(x₁, x₂)) = 0
POL(new_merge(x₁, x₂, x₃)) = x₁
POL(new_merge0(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₃
POL(new_primCmpNat0(x₁, x₂)) = 0
POL(new_primCmpNat1(x₁, x₂)) = 0
POL(new_primCmpNat2(x₁, x₂)) = 0
POL(new_primMulNat0(x₁, x₂)) = 0
POL(new_primPlusNat0(x₁, x₂)) = 0
POL(new_primPlusNat1(x₁, x₂)) = 1 + x₁
POL(new_sr(x₁, x₂)) = 1 + x₁
POL(new_sr0(x₁, x₂)) = 1
POL(ty_@0) = 0
POL(ty_@2) = 0
POL(ty_@3) = 0
POL(ty_Bool) = 0
POL(ty_Char) = 0
POL(ty_Double) = 0
POL(ty_Either) = 0
POL(ty_Float) = 0
POL(ty_Int) = 0
POL(ty_Integer) = 0
POL(ty_Maybe) = 0
POL(ty_Ordering) = 0
POL(ty_Ratio) = 0
POL(ty_[]) = 0

The following usable rules [17] were oriented: none

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz511, vz512, vz513, vz514, GT, ba) → new_merge(:(vz512, vz513), vz514, ba)
new_merge(:(vz5010, vz5011), :(vz50200, vz50201), bb) → new_merge0(vz50200, vz5010, vz5011, vz50201, new_compare(vz5010, vz50200, bb), bb)

The TRS R consists of the following rules:

new_sr(Neg(vz503000), Neg(vz504010)) → Pos(new_primMulNat0(vz503000, vz504010))
new_compare(vz5010, vz50200, app(ty_Ratio, ca)) → new_compare2(vz5010, vz50200, ca)
new_primCmpNat1(Succ(vz5010000), Succ(vz50200000)) → new_primCmpNat1(vz5010000, vz50200000)
new_compare3(Neg(Zero), Pos(Zero)) → EQ
new_compare3(Pos(Zero), Neg(Zero)) → EQ
new_compare10(vz5010, vz50200) → error([])
new_compare2(:%(vz50100, vz50101), :%(vz502000, vz502001), ty_Integer) → new_compare4(new_sr0(vz50100, vz502001), new_sr0(vz502000, vz50101))
new_primCmpNat2(Zero, vz501000) → LT
new_sr(Pos(vz503000), Pos(vz504010)) → Pos(new_primMulNat0(vz503000, vz504010))
new_compare(vz5010, vz50200, ty_Char) → new_compare1(vz5010, vz50200)
new_compare(vz5010, vz50200, ty_Bool) → new_compare6(vz5010, vz50200)
new_compare3(Neg(Zero), Pos(Succ(vz5020000))) → LT
new_primPlusNat1(Succ(vz51600), Succ(vz50401000)) → Succ(Succ(new_primPlusNat1(vz51600, vz50401000)))
new_sr0(vz502000, vz50101) → error([])
new_compare(vz5010, vz50200, ty_Float) → new_compare9(vz5010, vz50200)
new_primMulNat0(Zero, Succ(vz5040100)) → Zero
new_primMulNat0(Succ(vz5030000), Zero) → Zero
new_compare(vz5010, vz50200, ty_Int) → new_compare3(vz5010, vz50200)
new_primPlusNat1(Zero, Zero) → Zero
new_compare7(vz5010, vz50200, be) → error([])
new_primCmpNat1(Zero, Succ(vz50200000)) → LT
new_compare8(vz5010, vz50200, bf, bg) → error([])
new_primCmpNat2(Succ(vz5020000), vz501000) → new_primCmpNat1(vz5020000, vz501000)
new_compare(vz5010, vz50200, ty_Double) → new_compare12(vz5010, vz50200)
new_compare(vz5010, vz50200, app(app(app(ty_@3, cb), cc), cd)) → new_compare13(vz5010, vz50200, cb, cc, cd)
new_primMulNat0(Succ(vz5030000), Succ(vz5040100)) → new_primPlusNat0(new_primMulNat0(vz5030000, Succ(vz5040100)), vz5040100)
new_compare2(:%(vz50100, vz50101), :%(vz502000, vz502001), ty_Int) → new_compare3(new_sr(vz50100, vz502001), new_sr(vz502000, vz50101))
new_compare(vz5010, vz50200, app(app(ty_Either, bc), bd)) → new_compare0(vz5010, vz50200, bc, bd)
new_compare9(vz5010, vz50200) → error([])
new_compare(vz5010, vz50200, app(app(ty_@2, bf), bg)) → new_compare8(vz5010, vz50200, bf, bg)
new_compare0(vz5010, vz50200, bc, bd) → error([])
new_compare3(Pos(Zero), Pos(Succ(vz5020000))) → new_primCmpNat2(Zero, vz5020000)
new_compare3(Neg(Succ(vz501000)), Pos(vz502000)) → LT
new_primCmpNat1(Zero, Zero) → EQ
new_compare3(Pos(Zero), Pos(Zero)) → EQ
new_compare3(Pos(Succ(vz501000)), Pos(vz502000)) → new_primCmpNat0(vz501000, vz502000)
new_primCmpNat0(vz501000, Zero) → GT
new_primMulNat0(Zero, Zero) → Zero
new_compare4(vz5010, vz50200) → error([])
new_primPlusNat0(Succ(vz5160), vz5040100) → Succ(Succ(new_primPlusNat1(vz5160, vz5040100)))
new_compare11(vz5010, vz50200, bh) → error([])
new_compare(vz5010, vz50200, ty_Integer) → new_compare4(vz5010, vz50200)
new_compare(vz5010, vz50200, ty_@0) → new_compare5(vz5010, vz50200)
new_compare3(Neg(Succ(vz501000)), Neg(vz502000)) → new_primCmpNat2(vz502000, vz501000)
new_primPlusNat0(Zero, vz5040100) → Succ(vz5040100)
new_primCmpNat1(Succ(vz5010000), Zero) → GT
new_compare3(Neg(Zero), Neg(Succ(vz5020000))) → new_primCmpNat0(vz5020000, Zero)
new_compare1(vz5010, vz50200) → error([])
new_compare6(vz5010, vz50200) → error([])
new_compare5(vz5010, vz50200) → error([])
new_compare12(vz5010, vz50200) → error([])
new_compare(vz5010, vz50200, app(ty_Maybe, be)) → new_compare7(vz5010, vz50200, be)
new_primPlusNat1(Succ(vz51600), Zero) → Succ(vz51600)
new_primPlusNat1(Zero, Succ(vz50401000)) → Succ(vz50401000)
new_compare3(Pos(Zero), Neg(Succ(vz5020000))) → GT
new_sr(Pos(vz503000), Neg(vz504010)) → Neg(new_primMulNat0(vz503000, vz504010))
new_sr(Neg(vz503000), Pos(vz504010)) → Neg(new_primMulNat0(vz503000, vz504010))
new_compare(vz5010, vz50200, ty_Ordering) → new_compare10(vz5010, vz50200)
new_compare3(Neg(Zero), Neg(Zero)) → EQ
new_compare3(Pos(Succ(vz501000)), Neg(vz502000)) → GT
new_primCmpNat0(vz501000, Succ(vz5020000)) → new_primCmpNat1(vz501000, vz5020000)
new_compare13(vz5010, vz50200, cb, cc, cd) → error([])
new_compare(vz5010, vz50200, app(ty_[], bh)) → new_compare11(vz5010, vz50200, bh)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), x1)
new_primCmpNat0(x0, Succ(x1))
new_compare(x0, x1, ty_Bool)
new_compare0(x0, x1, x2, x3)
new_compare9(x0, x1)
new_compare(x0, x1, ty_Integer)
new_primMulNat0(Zero, Zero)
new_compare11(x0, x1, x2)
new_compare(x0, x1, ty_Char)
new_sr0(x0, x1)
new_compare12(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_compare1(x0, x1)
new_compare(x0, x1, ty_Float)
new_compare3(Pos(Succ(x0)), Pos(x1))
new_compare(x0, x1, ty_Ordering)
new_compare5(x0, x1)
new_compare10(x0, x1)
new_compare3(Neg(Zero), Neg(Succ(x0)))
new_primPlusNat1(Zero, Zero)
new_compare2(:%(x0, x1), :%(x2, x3), ty_Integer)
new_primCmpNat1(Zero, Zero)
new_primCmpNat1(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, Succ(x0))
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), Zero)
new_compare(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_primCmpNat2(Zero, x0)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare3(Pos(Zero), Pos(Succ(x0)))
new_compare3(Neg(Zero), Neg(Zero))
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare13(x0, x1, x2, x3, x4)
new_compare2(:%(x0, x1), :%(x2, x3), ty_Int)
new_primMulNat0(Succ(x0), Zero)
new_primCmpNat0(x0, Zero)
new_compare(x0, x1, app(ty_[], x2))
new_compare4(x0, x1)
new_sr(Pos(x0), Pos(x1))
new_compare3(Pos(Zero), Neg(Succ(x0)))
new_compare7(x0, x1, x2)
new_compare3(Neg(Zero), Pos(Succ(x0)))
new_compare3(Pos(Zero), Pos(Zero))
new_primCmpNat1(Succ(x0), Zero)
new_compare6(x0, x1)
new_compare3(Neg(Succ(x0)), Neg(x1))
new_primCmpNat2(Succ(x0), x1)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare8(x0, x1, x2, x3)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_sr(Neg(x0), Neg(x1))
new_compare3(Pos(Succ(x0)), Neg(x1))
new_compare3(Neg(Succ(x0)), Pos(x1))
new_primCmpNat1(Zero, Succ(x0))
new_compare3(Pos(Zero), Neg(Zero))
new_compare3(Neg(Zero), Pos(Zero))
new_primPlusNat1(Succ(x0), Succ(x1))
new_compare(x0, x1, ty_@0)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_merge(:(vz5010, vz5011), :(vz50200, vz50201), bb) → new_merge0(vz50200, vz5010, vz5011, vz50201, new_compare(vz5010, vz50200, bb), bb)
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4, 3 >= 6
new_merge0(vz511, vz512, vz513, vz514, GT, ba) → new_merge(:(vz512, vz513), vz514, ba)
The graph contains the following edges 4 >= 2, 6 >= 3

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge_pairs(:(vz502110, :(vz5021110, vz5021111)), ba) → new_merge_pairs(vz5021111, ba)

From the DPs we obtained the following set of size-change graphs:

new_merge_pairs(:(vz502110, :(vz5021110, vz5021111)), ba) → new_merge_pairs(vz5021111, ba)
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz501, :(vz5020, []), ba) → new_mergesort'(new_merge2(vz501, vz5020, ba), [], ba)
new_mergesort'(vz501, :(vz5020, :(vz50210, vz50211)), ba) → new_mergesort'(new_merge1(vz501, vz5020, vz50210, ba), new_merge_pairs0(vz50211, ba), ba)

The TRS R consists of the following rules:

new_sr(Neg(vz503000), Neg(vz504010)) → Pos(new_primMulNat0(vz503000, vz504010))
new_compare(vz5010, vz50200, app(ty_Ratio, cb)) → new_compare2(vz5010, vz50200, cb)
new_primCmpNat1(Succ(vz5010000), Succ(vz50200000)) → new_primCmpNat1(vz5010000, vz50200000)
new_compare2(:%(vz50100, vz50101), :%(vz502000, vz502001), ty_Integer) → new_compare4(new_sr0(vz50100, vz502001), new_sr0(vz502000, vz50101))
new_compare10(vz5010, vz50200) → error([])
new_compare3(Pos(Zero), Neg(Zero)) → EQ
new_compare3(Neg(Zero), Pos(Zero)) → EQ
new_sr(Pos(vz503000), Pos(vz504010)) → Pos(new_primMulNat0(vz503000, vz504010))
new_primCmpNat2(Zero, vz501000) → LT
new_merge00(vz511, vz512, vz513, vz514, LT, cd) → :(vz512, new_merge2(vz513, :(vz511, vz514), cd))
new_compare14(vz50200, vz502100, ty_Int) → new_compare3(vz50200, vz502100)
new_compare14(vz50200, vz502100, app(app(ty_@2, be), bf)) → new_compare8(vz50200, vz502100, be, bf)
new_compare(vz5010, vz50200, ty_Char) → new_compare1(vz5010, vz50200)
new_compare(vz5010, vz50200, ty_Bool) → new_compare6(vz5010, vz50200)
new_primPlusNat1(Succ(vz51600), Succ(vz50401000)) → Succ(Succ(new_primPlusNat1(vz51600, vz50401000)))
new_merge_pairs0(:(vz502110, :(vz5021110, vz5021111)), ba) → :(new_merge2(vz502110, vz5021110, ba), new_merge_pairs0(vz5021111, ba))
new_compare3(Neg(Zero), Pos(Succ(vz5020000))) → LT
new_compare14(vz50200, vz502100, ty_Char) → new_compare1(vz50200, vz502100)
new_sr0(vz502000, vz50101) → error([])
new_merge1(vz501, [], :(vz502100, vz502101), ba) → new_merge2(vz501, :(vz502100, vz502101), ba)
new_compare(vz5010, vz50200, ty_Float) → new_compare9(vz5010, vz50200)
new_merge_pairs0(:(vz502110, []), ba) → :(vz502110, [])
new_primMulNat0(Zero, Succ(vz5040100)) → Zero
new_primMulNat0(Succ(vz5030000), Zero) → Zero
new_compare(vz5010, vz50200, ty_Int) → new_compare3(vz5010, vz50200)
new_merge1(vz501, :(vz50200, vz50201), :(vz502100, vz502101), ba) → new_merge2(vz501, new_merge00(vz502100, vz50200, vz50201, vz502101, new_compare14(vz50200, vz502100, ba), ba), ba)
new_primPlusNat1(Zero, Zero) → Zero
new_compare14(vz50200, vz502100, ty_Ordering) → new_compare10(vz50200, vz502100)
new_compare7(vz5010, vz50200, bd) → error([])
new_primCmpNat1(Zero, Succ(vz50200000)) → LT
new_merge00(vz511, vz512, vz513, vz514, GT, cd) → :(vz511, new_merge2(:(vz512, vz513), vz514, cd))
new_compare8(vz5010, vz50200, be, bf) → error([])
new_primCmpNat2(Succ(vz5020000), vz501000) → new_primCmpNat1(vz5020000, vz501000)
new_compare(vz5010, vz50200, ty_Double) → new_compare12(vz5010, vz50200)
new_compare(vz5010, vz50200, app(app(app(ty_@3, bg), bh), ca)) → new_compare13(vz5010, vz50200, bg, bh, ca)
new_primMulNat0(Succ(vz5030000), Succ(vz5040100)) → new_primPlusNat0(new_primMulNat0(vz5030000, Succ(vz5040100)), vz5040100)
new_compare2(:%(vz50100, vz50101), :%(vz502000, vz502001), ty_Int) → new_compare3(new_sr(vz50100, vz502001), new_sr(vz502000, vz50101))
new_compare(vz5010, vz50200, app(app(ty_Either, bb), bc)) → new_compare0(vz5010, vz50200, bb, bc)
new_compare9(vz5010, vz50200) → error([])
new_compare(vz5010, vz50200, app(app(ty_@2, be), bf)) → new_compare8(vz5010, vz50200, be, bf)
new_compare0(vz5010, vz50200, bb, bc) → error([])
new_compare14(vz50200, vz502100, app(app(ty_Either, bb), bc)) → new_compare0(vz50200, vz502100, bb, bc)
new_compare14(vz50200, vz502100, app(ty_Maybe, bd)) → new_compare7(vz50200, vz502100, bd)
new_compare3(Pos(Zero), Pos(Succ(vz5020000))) → new_primCmpNat2(Zero, vz5020000)
new_compare3(Neg(Succ(vz501000)), Pos(vz502000)) → LT
new_primCmpNat1(Zero, Zero) → EQ
new_primCmpNat0(vz501000, Zero) → GT
new_compare3(Pos(Succ(vz501000)), Pos(vz502000)) → new_primCmpNat0(vz501000, vz502000)
new_compare3(Pos(Zero), Pos(Zero)) → EQ
new_merge2([], :(vz50200, vz50201), ba) → :(vz50200, vz50201)
new_primMulNat0(Zero, Zero) → Zero
new_merge_pairs0([], ba) → []
new_compare4(vz5010, vz50200) → error([])
new_primPlusNat0(Succ(vz5160), vz5040100) → Succ(Succ(new_primPlusNat1(vz5160, vz5040100)))
new_compare(vz5010, vz50200, ty_Integer) → new_compare4(vz5010, vz50200)
new_compare11(vz5010, vz50200, cc) → error([])
new_merge1(vz501, vz5020, [], ba) → new_merge2(vz501, vz5020, ba)
new_merge2(:(vz5010, vz5011), :(vz50200, vz50201), ba) → new_merge00(vz50200, vz5010, vz5011, vz50201, new_compare(vz5010, vz50200, ba), ba)
new_compare14(vz50200, vz502100, app(ty_[], cc)) → new_compare11(vz50200, vz502100, cc)
new_compare(vz5010, vz50200, ty_@0) → new_compare5(vz5010, vz50200)
new_primPlusNat0(Zero, vz5040100) → Succ(vz5040100)
new_compare3(Neg(Succ(vz501000)), Neg(vz502000)) → new_primCmpNat2(vz502000, vz501000)
new_merge2(vz501, [], ba) → vz501
new_primCmpNat1(Succ(vz5010000), Zero) → GT
new_compare3(Neg(Zero), Neg(Succ(vz5020000))) → new_primCmpNat0(vz5020000, Zero)
new_compare14(vz50200, vz502100, ty_Double) → new_compare12(vz50200, vz502100)
new_compare1(vz5010, vz50200) → error([])
new_compare6(vz5010, vz50200) → error([])
new_compare14(vz50200, vz502100, ty_Float) → new_compare9(vz50200, vz502100)
new_compare5(vz5010, vz50200) → error([])
new_compare12(vz5010, vz50200) → error([])
new_compare(vz5010, vz50200, app(ty_Maybe, bd)) → new_compare7(vz5010, vz50200, bd)
new_primPlusNat1(Succ(vz51600), Zero) → Succ(vz51600)
new_primPlusNat1(Zero, Succ(vz50401000)) → Succ(vz50401000)
new_compare3(Pos(Zero), Neg(Succ(vz5020000))) → GT
new_sr(Neg(vz503000), Pos(vz504010)) → Neg(new_primMulNat0(vz503000, vz504010))
new_sr(Pos(vz503000), Neg(vz504010)) → Neg(new_primMulNat0(vz503000, vz504010))
new_compare14(vz50200, vz502100, ty_Bool) → new_compare6(vz50200, vz502100)
new_compare(vz5010, vz50200, ty_Ordering) → new_compare10(vz5010, vz50200)
new_merge00(vz511, vz512, vz513, vz514, EQ, cd) → :(vz512, new_merge2(vz513, :(vz511, vz514), cd))
new_compare14(vz50200, vz502100, app(ty_Ratio, cb)) → new_compare2(vz50200, vz502100, cb)
new_compare14(vz50200, vz502100, app(app(app(ty_@3, bg), bh), ca)) → new_compare13(vz50200, vz502100, bg, bh, ca)
new_compare3(Pos(Succ(vz501000)), Neg(vz502000)) → GT
new_compare3(Neg(Zero), Neg(Zero)) → EQ
new_primCmpNat0(vz501000, Succ(vz5020000)) → new_primCmpNat1(vz501000, vz5020000)
new_compare14(vz50200, vz502100, ty_Integer) → new_compare4(vz50200, vz502100)
new_compare13(vz5010, vz50200, bg, bh, ca) → error([])
new_compare(vz5010, vz50200, app(ty_[], cc)) → new_compare11(vz5010, vz50200, cc)
new_compare14(vz50200, vz502100, ty_@0) → new_compare5(vz50200, vz502100)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), x1)
new_compare14(x0, x1, ty_Double)
new_primCmpNat0(x0, Succ(x1))
new_merge2([], :(x0, x1), x2)
new_compare(x0, x1, ty_Bool)
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare(x0, x1, ty_Integer)
new_compare9(x0, x1)
new_merge1(x0, x1, [], x2)
new_primMulNat0(Zero, Zero)
new_compare(x0, x1, ty_Char)
new_sr0(x0, x1)
new_compare14(x0, x1, app(ty_[], x2))
new_compare12(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare1(x0, x1)
new_compare(x0, x1, ty_Float)
new_compare14(x0, x1, ty_Ordering)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare3(Pos(Succ(x0)), Pos(x1))
new_compare(x0, x1, ty_Ordering)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare5(x0, x1)
new_compare10(x0, x1)
new_compare3(Neg(Zero), Neg(Succ(x0)))
new_compare7(x0, x1, x2)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Zero)
new_merge00(x0, x1, x2, x3, LT, x4)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare2(:%(x0, x1), :%(x2, x3), ty_Integer)
new_compare14(x0, x1, ty_Float)
new_compare(x0, x1, app(ty_Ratio, x2))
new_primCmpNat1(Zero, Zero)
new_compare13(x0, x1, x2, x3, x4)
new_primCmpNat1(Succ(x0), Succ(x1))
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare14(x0, x1, app(ty_Maybe, x2))
new_merge_pairs0([], x0)
new_primPlusNat1(Zero, Succ(x0))
new_compare8(x0, x1, x2, x3)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), Zero)
new_compare(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_merge1(x0, [], :(x1, x2), x3)
new_compare14(x0, x1, ty_@0)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, ty_Char)
new_primCmpNat2(Zero, x0)
new_compare14(x0, x1, ty_Int)
new_compare3(Pos(Zero), Pos(Succ(x0)))
new_compare3(Neg(Zero), Neg(Zero))
new_compare(x0, x1, app(ty_[], x2))
new_compare11(x0, x1, x2)
new_compare0(x0, x1, x2, x3)
new_compare2(:%(x0, x1), :%(x2, x3), ty_Int)
new_primMulNat0(Succ(x0), Zero)
new_merge2(x0, [], x1)
new_primCmpNat0(x0, Zero)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare4(x0, x1)
new_compare14(x0, x1, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_compare3(Pos(Zero), Neg(Succ(x0)))
new_primCmpNat1(Succ(x0), Zero)
new_compare3(Neg(Zero), Pos(Succ(x0)))
new_compare3(Pos(Zero), Pos(Zero))
new_compare6(x0, x1)
new_compare3(Neg(Succ(x0)), Neg(x1))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpNat2(Succ(x0), x1)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Neg(x1))
new_compare3(Pos(Succ(x0)), Neg(x1))
new_compare3(Neg(Succ(x0)), Pos(x1))
new_compare14(x0, x1, ty_Integer)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_merge_pairs0(:(x0, []), x1)
new_primCmpNat1(Zero, Succ(x0))
new_compare(x0, x1, ty_@0)
new_primPlusNat1(Succ(x0), Succ(x1))
new_compare3(Neg(Zero), Pos(Zero))
new_compare3(Pos(Zero), Neg(Zero))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz501, :(vz5020, :(vz50210, vz50211)), ba) → new_mergesort'(new_merge1(vz501, vz5020, vz50210, ba), new_merge_pairs0(vz50211, ba), ba)

The TRS R consists of the following rules:

new_sr(Neg(vz503000), Neg(vz504010)) → Pos(new_primMulNat0(vz503000, vz504010))
new_compare(vz5010, vz50200, app(ty_Ratio, cb)) → new_compare2(vz5010, vz50200, cb)
new_primCmpNat1(Succ(vz5010000), Succ(vz50200000)) → new_primCmpNat1(vz5010000, vz50200000)
new_compare2(:%(vz50100, vz50101), :%(vz502000, vz502001), ty_Integer) → new_compare4(new_sr0(vz50100, vz502001), new_sr0(vz502000, vz50101))
new_compare10(vz5010, vz50200) → error([])
new_compare3(Pos(Zero), Neg(Zero)) → EQ
new_compare3(Neg(Zero), Pos(Zero)) → EQ
new_sr(Pos(vz503000), Pos(vz504010)) → Pos(new_primMulNat0(vz503000, vz504010))
new_primCmpNat2(Zero, vz501000) → LT
new_merge00(vz511, vz512, vz513, vz514, LT, cd) → :(vz512, new_merge2(vz513, :(vz511, vz514), cd))
new_compare14(vz50200, vz502100, ty_Int) → new_compare3(vz50200, vz502100)
new_compare14(vz50200, vz502100, app(app(ty_@2, be), bf)) → new_compare8(vz50200, vz502100, be, bf)
new_compare(vz5010, vz50200, ty_Char) → new_compare1(vz5010, vz50200)
new_compare(vz5010, vz50200, ty_Bool) → new_compare6(vz5010, vz50200)
new_primPlusNat1(Succ(vz51600), Succ(vz50401000)) → Succ(Succ(new_primPlusNat1(vz51600, vz50401000)))
new_merge_pairs0(:(vz502110, :(vz5021110, vz5021111)), ba) → :(new_merge2(vz502110, vz5021110, ba), new_merge_pairs0(vz5021111, ba))
new_compare3(Neg(Zero), Pos(Succ(vz5020000))) → LT
new_compare14(vz50200, vz502100, ty_Char) → new_compare1(vz50200, vz502100)
new_sr0(vz502000, vz50101) → error([])
new_merge1(vz501, [], :(vz502100, vz502101), ba) → new_merge2(vz501, :(vz502100, vz502101), ba)
new_compare(vz5010, vz50200, ty_Float) → new_compare9(vz5010, vz50200)
new_merge_pairs0(:(vz502110, []), ba) → :(vz502110, [])
new_primMulNat0(Zero, Succ(vz5040100)) → Zero
new_primMulNat0(Succ(vz5030000), Zero) → Zero
new_compare(vz5010, vz50200, ty_Int) → new_compare3(vz5010, vz50200)
new_merge1(vz501, :(vz50200, vz50201), :(vz502100, vz502101), ba) → new_merge2(vz501, new_merge00(vz502100, vz50200, vz50201, vz502101, new_compare14(vz50200, vz502100, ba), ba), ba)
new_primPlusNat1(Zero, Zero) → Zero
new_compare14(vz50200, vz502100, ty_Ordering) → new_compare10(vz50200, vz502100)
new_compare7(vz5010, vz50200, bd) → error([])
new_primCmpNat1(Zero, Succ(vz50200000)) → LT
new_merge00(vz511, vz512, vz513, vz514, GT, cd) → :(vz511, new_merge2(:(vz512, vz513), vz514, cd))
new_compare8(vz5010, vz50200, be, bf) → error([])
new_primCmpNat2(Succ(vz5020000), vz501000) → new_primCmpNat1(vz5020000, vz501000)
new_compare(vz5010, vz50200, ty_Double) → new_compare12(vz5010, vz50200)
new_compare(vz5010, vz50200, app(app(app(ty_@3, bg), bh), ca)) → new_compare13(vz5010, vz50200, bg, bh, ca)
new_primMulNat0(Succ(vz5030000), Succ(vz5040100)) → new_primPlusNat0(new_primMulNat0(vz5030000, Succ(vz5040100)), vz5040100)
new_compare2(:%(vz50100, vz50101), :%(vz502000, vz502001), ty_Int) → new_compare3(new_sr(vz50100, vz502001), new_sr(vz502000, vz50101))
new_compare(vz5010, vz50200, app(app(ty_Either, bb), bc)) → new_compare0(vz5010, vz50200, bb, bc)
new_compare9(vz5010, vz50200) → error([])
new_compare(vz5010, vz50200, app(app(ty_@2, be), bf)) → new_compare8(vz5010, vz50200, be, bf)
new_compare0(vz5010, vz50200, bb, bc) → error([])
new_compare14(vz50200, vz502100, app(app(ty_Either, bb), bc)) → new_compare0(vz50200, vz502100, bb, bc)
new_compare14(vz50200, vz502100, app(ty_Maybe, bd)) → new_compare7(vz50200, vz502100, bd)
new_compare3(Pos(Zero), Pos(Succ(vz5020000))) → new_primCmpNat2(Zero, vz5020000)
new_compare3(Neg(Succ(vz501000)), Pos(vz502000)) → LT
new_primCmpNat1(Zero, Zero) → EQ
new_primCmpNat0(vz501000, Zero) → GT
new_compare3(Pos(Succ(vz501000)), Pos(vz502000)) → new_primCmpNat0(vz501000, vz502000)
new_compare3(Pos(Zero), Pos(Zero)) → EQ
new_merge2([], :(vz50200, vz50201), ba) → :(vz50200, vz50201)
new_primMulNat0(Zero, Zero) → Zero
new_merge_pairs0([], ba) → []
new_compare4(vz5010, vz50200) → error([])
new_primPlusNat0(Succ(vz5160), vz5040100) → Succ(Succ(new_primPlusNat1(vz5160, vz5040100)))
new_compare(vz5010, vz50200, ty_Integer) → new_compare4(vz5010, vz50200)
new_compare11(vz5010, vz50200, cc) → error([])
new_merge1(vz501, vz5020, [], ba) → new_merge2(vz501, vz5020, ba)
new_merge2(:(vz5010, vz5011), :(vz50200, vz50201), ba) → new_merge00(vz50200, vz5010, vz5011, vz50201, new_compare(vz5010, vz50200, ba), ba)
new_compare14(vz50200, vz502100, app(ty_[], cc)) → new_compare11(vz50200, vz502100, cc)
new_compare(vz5010, vz50200, ty_@0) → new_compare5(vz5010, vz50200)
new_primPlusNat0(Zero, vz5040100) → Succ(vz5040100)
new_compare3(Neg(Succ(vz501000)), Neg(vz502000)) → new_primCmpNat2(vz502000, vz501000)
new_merge2(vz501, [], ba) → vz501
new_primCmpNat1(Succ(vz5010000), Zero) → GT
new_compare3(Neg(Zero), Neg(Succ(vz5020000))) → new_primCmpNat0(vz5020000, Zero)
new_compare14(vz50200, vz502100, ty_Double) → new_compare12(vz50200, vz502100)
new_compare1(vz5010, vz50200) → error([])
new_compare6(vz5010, vz50200) → error([])
new_compare14(vz50200, vz502100, ty_Float) → new_compare9(vz50200, vz502100)
new_compare5(vz5010, vz50200) → error([])
new_compare12(vz5010, vz50200) → error([])
new_compare(vz5010, vz50200, app(ty_Maybe, bd)) → new_compare7(vz5010, vz50200, bd)
new_primPlusNat1(Succ(vz51600), Zero) → Succ(vz51600)
new_primPlusNat1(Zero, Succ(vz50401000)) → Succ(vz50401000)
new_compare3(Pos(Zero), Neg(Succ(vz5020000))) → GT
new_sr(Neg(vz503000), Pos(vz504010)) → Neg(new_primMulNat0(vz503000, vz504010))
new_sr(Pos(vz503000), Neg(vz504010)) → Neg(new_primMulNat0(vz503000, vz504010))
new_compare14(vz50200, vz502100, ty_Bool) → new_compare6(vz50200, vz502100)
new_compare(vz5010, vz50200, ty_Ordering) → new_compare10(vz5010, vz50200)
new_merge00(vz511, vz512, vz513, vz514, EQ, cd) → :(vz512, new_merge2(vz513, :(vz511, vz514), cd))
new_compare14(vz50200, vz502100, app(ty_Ratio, cb)) → new_compare2(vz50200, vz502100, cb)
new_compare14(vz50200, vz502100, app(app(app(ty_@3, bg), bh), ca)) → new_compare13(vz50200, vz502100, bg, bh, ca)
new_compare3(Pos(Succ(vz501000)), Neg(vz502000)) → GT
new_compare3(Neg(Zero), Neg(Zero)) → EQ
new_primCmpNat0(vz501000, Succ(vz5020000)) → new_primCmpNat1(vz501000, vz5020000)
new_compare14(vz50200, vz502100, ty_Integer) → new_compare4(vz50200, vz502100)
new_compare13(vz5010, vz50200, bg, bh, ca) → error([])
new_compare(vz5010, vz50200, app(ty_[], cc)) → new_compare11(vz5010, vz50200, cc)
new_compare14(vz50200, vz502100, ty_@0) → new_compare5(vz50200, vz502100)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), x1)
new_compare14(x0, x1, ty_Double)
new_primCmpNat0(x0, Succ(x1))
new_merge2([], :(x0, x1), x2)
new_compare(x0, x1, ty_Bool)
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare(x0, x1, ty_Integer)
new_compare9(x0, x1)
new_merge1(x0, x1, [], x2)
new_primMulNat0(Zero, Zero)
new_compare(x0, x1, ty_Char)
new_sr0(x0, x1)
new_compare14(x0, x1, app(ty_[], x2))
new_compare12(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare1(x0, x1)
new_compare(x0, x1, ty_Float)
new_compare14(x0, x1, ty_Ordering)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare3(Pos(Succ(x0)), Pos(x1))
new_compare(x0, x1, ty_Ordering)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare5(x0, x1)
new_compare10(x0, x1)
new_compare3(Neg(Zero), Neg(Succ(x0)))
new_compare7(x0, x1, x2)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Zero)
new_merge00(x0, x1, x2, x3, LT, x4)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare2(:%(x0, x1), :%(x2, x3), ty_Integer)
new_compare14(x0, x1, ty_Float)
new_compare(x0, x1, app(ty_Ratio, x2))
new_primCmpNat1(Zero, Zero)
new_compare13(x0, x1, x2, x3, x4)
new_primCmpNat1(Succ(x0), Succ(x1))
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare14(x0, x1, app(ty_Maybe, x2))
new_merge_pairs0([], x0)
new_primPlusNat1(Zero, Succ(x0))
new_compare8(x0, x1, x2, x3)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), Zero)
new_compare(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_merge1(x0, [], :(x1, x2), x3)
new_compare14(x0, x1, ty_@0)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, ty_Char)
new_primCmpNat2(Zero, x0)
new_compare14(x0, x1, ty_Int)
new_compare3(Pos(Zero), Pos(Succ(x0)))
new_compare3(Neg(Zero), Neg(Zero))
new_compare(x0, x1, app(ty_[], x2))
new_compare11(x0, x1, x2)
new_compare0(x0, x1, x2, x3)
new_compare2(:%(x0, x1), :%(x2, x3), ty_Int)
new_primMulNat0(Succ(x0), Zero)
new_merge2(x0, [], x1)
new_primCmpNat0(x0, Zero)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare4(x0, x1)
new_compare14(x0, x1, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_compare3(Pos(Zero), Neg(Succ(x0)))
new_primCmpNat1(Succ(x0), Zero)
new_compare3(Neg(Zero), Pos(Succ(x0)))
new_compare3(Pos(Zero), Pos(Zero))
new_compare6(x0, x1)
new_compare3(Neg(Succ(x0)), Neg(x1))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpNat2(Succ(x0), x1)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Neg(x1))
new_compare3(Pos(Succ(x0)), Neg(x1))
new_compare3(Neg(Succ(x0)), Pos(x1))
new_compare14(x0, x1, ty_Integer)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_merge_pairs0(:(x0, []), x1)
new_primCmpNat1(Zero, Succ(x0))
new_compare(x0, x1, ty_@0)
new_primPlusNat1(Succ(x0), Succ(x1))
new_compare3(Neg(Zero), Pos(Zero))
new_compare3(Pos(Zero), Neg(Zero))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_mergesort'(vz501, :(vz5020, :(vz50210, vz50211)), ba) → new_mergesort'(new_merge1(vz501, vz5020, vz50210, ba), new_merge_pairs0(vz50211, ba), ba)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₂
POL(:%(x₁, x₂)) = 1 + x₁ + x₂
POL(EQ) = 0
POL(GT) = 0
POL(LT) = 0
POL(Neg(x₁)) = 1 + x₁
POL(Pos(x₁)) = x₁
POL(Succ(x₁)) = x₁
POL(Zero) = 0
POL([]) = 0
POL(app(x₁, x₂)) = 1 + x₁ + x₂
POL(error(x₁)) = 0
POL(new_compare(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(new_compare0(x₁, x₂, x₃, x₄)) = 1
POL(new_compare1(x₁, x₂)) = 1
POL(new_compare10(x₁, x₂)) = 1
POL(new_compare11(x₁, x₂, x₃)) = 1
POL(new_compare12(x₁, x₂)) = 1
POL(new_compare13(x₁, x₂, x₃, x₄, x₅)) = 1 + x₃
POL(new_compare14(x₁, x₂, x₃)) = 0
POL(new_compare2(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(new_compare3(x₁, x₂)) = x₁
POL(new_compare4(x₁, x₂)) = 1
POL(new_compare5(x₁, x₂)) = 1
POL(new_compare6(x₁, x₂)) = 1
POL(new_compare7(x₁, x₂, x₃)) = 1 + x₃
POL(new_compare8(x₁, x₂, x₃, x₄)) = 1
POL(new_compare9(x₁, x₂)) = 0
POL(new_merge00(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(new_merge1(x₁, x₂, x₃, x₄)) = 0
POL(new_merge2(x₁, x₂, x₃)) = 0
POL(new_merge_pairs0(x₁, x₂)) = 1 + x₁
POL(new_mergesort'(x₁, x₂, x₃)) = x₂
POL(new_primCmpNat0(x₁, x₂)) = 0
POL(new_primCmpNat1(x₁, x₂)) = 0
POL(new_primCmpNat2(x₁, x₂)) = 0
POL(new_primMulNat0(x₁, x₂)) = 0
POL(new_primPlusNat0(x₁, x₂)) = 0
POL(new_primPlusNat1(x₁, x₂)) = 1 + x₁ + x₂
POL(new_sr(x₁, x₂)) = 1
POL(new_sr0(x₁, x₂)) = 1
POL(ty_@0) = 1
POL(ty_@2) = 1
POL(ty_@3) = 0
POL(ty_Bool) = 1
POL(ty_Char) = 1
POL(ty_Double) = 0
POL(ty_Either) = 1
POL(ty_Float) = 0
POL(ty_Int) = 1
POL(ty_Integer) = 1
POL(ty_Maybe) = 0
POL(ty_Ordering) = 1
POL(ty_Ratio) = 0
POL(ty_[]) = 0

The following usable rules [17] were oriented:

new_merge_pairs0([], ba) → []
new_merge_pairs0(:(vz502110, []), ba) → :(vz502110, [])
new_merge_pairs0(:(vz502110, :(vz5021110, vz5021111)), ba) → :(new_merge2(vz502110, vz5021110, ba), new_merge_pairs0(vz5021111, ba))

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_sr(Neg(vz503000), Neg(vz504010)) → Pos(new_primMulNat0(vz503000, vz504010))
new_compare(vz5010, vz50200, app(ty_Ratio, cb)) → new_compare2(vz5010, vz50200, cb)
new_primCmpNat1(Succ(vz5010000), Succ(vz50200000)) → new_primCmpNat1(vz5010000, vz50200000)
new_compare2(:%(vz50100, vz50101), :%(vz502000, vz502001), ty_Integer) → new_compare4(new_sr0(vz50100, vz502001), new_sr0(vz502000, vz50101))
new_compare10(vz5010, vz50200) → error([])
new_compare3(Pos(Zero), Neg(Zero)) → EQ
new_compare3(Neg(Zero), Pos(Zero)) → EQ
new_sr(Pos(vz503000), Pos(vz504010)) → Pos(new_primMulNat0(vz503000, vz504010))
new_primCmpNat2(Zero, vz501000) → LT
new_merge00(vz511, vz512, vz513, vz514, LT, cd) → :(vz512, new_merge2(vz513, :(vz511, vz514), cd))
new_compare14(vz50200, vz502100, ty_Int) → new_compare3(vz50200, vz502100)
new_compare14(vz50200, vz502100, app(app(ty_@2, be), bf)) → new_compare8(vz50200, vz502100, be, bf)
new_compare(vz5010, vz50200, ty_Char) → new_compare1(vz5010, vz50200)
new_compare(vz5010, vz50200, ty_Bool) → new_compare6(vz5010, vz50200)
new_primPlusNat1(Succ(vz51600), Succ(vz50401000)) → Succ(Succ(new_primPlusNat1(vz51600, vz50401000)))
new_merge_pairs0(:(vz502110, :(vz5021110, vz5021111)), ba) → :(new_merge2(vz502110, vz5021110, ba), new_merge_pairs0(vz5021111, ba))
new_compare3(Neg(Zero), Pos(Succ(vz5020000))) → LT
new_compare14(vz50200, vz502100, ty_Char) → new_compare1(vz50200, vz502100)
new_sr0(vz502000, vz50101) → error([])
new_merge1(vz501, [], :(vz502100, vz502101), ba) → new_merge2(vz501, :(vz502100, vz502101), ba)
new_compare(vz5010, vz50200, ty_Float) → new_compare9(vz5010, vz50200)
new_merge_pairs0(:(vz502110, []), ba) → :(vz502110, [])
new_primMulNat0(Zero, Succ(vz5040100)) → Zero
new_primMulNat0(Succ(vz5030000), Zero) → Zero
new_compare(vz5010, vz50200, ty_Int) → new_compare3(vz5010, vz50200)
new_merge1(vz501, :(vz50200, vz50201), :(vz502100, vz502101), ba) → new_merge2(vz501, new_merge00(vz502100, vz50200, vz50201, vz502101, new_compare14(vz50200, vz502100, ba), ba), ba)
new_primPlusNat1(Zero, Zero) → Zero
new_compare14(vz50200, vz502100, ty_Ordering) → new_compare10(vz50200, vz502100)
new_compare7(vz5010, vz50200, bd) → error([])
new_primCmpNat1(Zero, Succ(vz50200000)) → LT
new_merge00(vz511, vz512, vz513, vz514, GT, cd) → :(vz511, new_merge2(:(vz512, vz513), vz514, cd))
new_compare8(vz5010, vz50200, be, bf) → error([])
new_primCmpNat2(Succ(vz5020000), vz501000) → new_primCmpNat1(vz5020000, vz501000)
new_compare(vz5010, vz50200, ty_Double) → new_compare12(vz5010, vz50200)
new_compare(vz5010, vz50200, app(app(app(ty_@3, bg), bh), ca)) → new_compare13(vz5010, vz50200, bg, bh, ca)
new_primMulNat0(Succ(vz5030000), Succ(vz5040100)) → new_primPlusNat0(new_primMulNat0(vz5030000, Succ(vz5040100)), vz5040100)
new_compare2(:%(vz50100, vz50101), :%(vz502000, vz502001), ty_Int) → new_compare3(new_sr(vz50100, vz502001), new_sr(vz502000, vz50101))
new_compare(vz5010, vz50200, app(app(ty_Either, bb), bc)) → new_compare0(vz5010, vz50200, bb, bc)
new_compare9(vz5010, vz50200) → error([])
new_compare(vz5010, vz50200, app(app(ty_@2, be), bf)) → new_compare8(vz5010, vz50200, be, bf)
new_compare0(vz5010, vz50200, bb, bc) → error([])
new_compare14(vz50200, vz502100, app(app(ty_Either, bb), bc)) → new_compare0(vz50200, vz502100, bb, bc)
new_compare14(vz50200, vz502100, app(ty_Maybe, bd)) → new_compare7(vz50200, vz502100, bd)
new_compare3(Pos(Zero), Pos(Succ(vz5020000))) → new_primCmpNat2(Zero, vz5020000)
new_compare3(Neg(Succ(vz501000)), Pos(vz502000)) → LT
new_primCmpNat1(Zero, Zero) → EQ
new_primCmpNat0(vz501000, Zero) → GT
new_compare3(Pos(Succ(vz501000)), Pos(vz502000)) → new_primCmpNat0(vz501000, vz502000)
new_compare3(Pos(Zero), Pos(Zero)) → EQ
new_merge2([], :(vz50200, vz50201), ba) → :(vz50200, vz50201)
new_primMulNat0(Zero, Zero) → Zero
new_merge_pairs0([], ba) → []
new_compare4(vz5010, vz50200) → error([])
new_primPlusNat0(Succ(vz5160), vz5040100) → Succ(Succ(new_primPlusNat1(vz5160, vz5040100)))
new_compare(vz5010, vz50200, ty_Integer) → new_compare4(vz5010, vz50200)
new_compare11(vz5010, vz50200, cc) → error([])
new_merge1(vz501, vz5020, [], ba) → new_merge2(vz501, vz5020, ba)
new_merge2(:(vz5010, vz5011), :(vz50200, vz50201), ba) → new_merge00(vz50200, vz5010, vz5011, vz50201, new_compare(vz5010, vz50200, ba), ba)
new_compare14(vz50200, vz502100, app(ty_[], cc)) → new_compare11(vz50200, vz502100, cc)
new_compare(vz5010, vz50200, ty_@0) → new_compare5(vz5010, vz50200)
new_primPlusNat0(Zero, vz5040100) → Succ(vz5040100)
new_compare3(Neg(Succ(vz501000)), Neg(vz502000)) → new_primCmpNat2(vz502000, vz501000)
new_merge2(vz501, [], ba) → vz501
new_primCmpNat1(Succ(vz5010000), Zero) → GT
new_compare3(Neg(Zero), Neg(Succ(vz5020000))) → new_primCmpNat0(vz5020000, Zero)
new_compare14(vz50200, vz502100, ty_Double) → new_compare12(vz50200, vz502100)
new_compare1(vz5010, vz50200) → error([])
new_compare6(vz5010, vz50200) → error([])
new_compare14(vz50200, vz502100, ty_Float) → new_compare9(vz50200, vz502100)
new_compare5(vz5010, vz50200) → error([])
new_compare12(vz5010, vz50200) → error([])
new_compare(vz5010, vz50200, app(ty_Maybe, bd)) → new_compare7(vz5010, vz50200, bd)
new_primPlusNat1(Succ(vz51600), Zero) → Succ(vz51600)
new_primPlusNat1(Zero, Succ(vz50401000)) → Succ(vz50401000)
new_compare3(Pos(Zero), Neg(Succ(vz5020000))) → GT
new_sr(Neg(vz503000), Pos(vz504010)) → Neg(new_primMulNat0(vz503000, vz504010))
new_sr(Pos(vz503000), Neg(vz504010)) → Neg(new_primMulNat0(vz503000, vz504010))
new_compare14(vz50200, vz502100, ty_Bool) → new_compare6(vz50200, vz502100)
new_compare(vz5010, vz50200, ty_Ordering) → new_compare10(vz5010, vz50200)
new_merge00(vz511, vz512, vz513, vz514, EQ, cd) → :(vz512, new_merge2(vz513, :(vz511, vz514), cd))
new_compare14(vz50200, vz502100, app(ty_Ratio, cb)) → new_compare2(vz50200, vz502100, cb)
new_compare14(vz50200, vz502100, app(app(app(ty_@3, bg), bh), ca)) → new_compare13(vz50200, vz502100, bg, bh, ca)
new_compare3(Pos(Succ(vz501000)), Neg(vz502000)) → GT
new_compare3(Neg(Zero), Neg(Zero)) → EQ
new_primCmpNat0(vz501000, Succ(vz5020000)) → new_primCmpNat1(vz501000, vz5020000)
new_compare14(vz50200, vz502100, ty_Integer) → new_compare4(vz50200, vz502100)
new_compare13(vz5010, vz50200, bg, bh, ca) → error([])
new_compare(vz5010, vz50200, app(ty_[], cc)) → new_compare11(vz5010, vz50200, cc)
new_compare14(vz50200, vz502100, ty_@0) → new_compare5(vz50200, vz502100)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), x1)
new_compare14(x0, x1, ty_Double)
new_primCmpNat0(x0, Succ(x1))
new_merge2([], :(x0, x1), x2)
new_compare(x0, x1, ty_Bool)
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare(x0, x1, ty_Integer)
new_compare9(x0, x1)
new_merge1(x0, x1, [], x2)
new_primMulNat0(Zero, Zero)
new_compare(x0, x1, ty_Char)
new_sr0(x0, x1)
new_compare14(x0, x1, app(ty_[], x2))
new_compare12(x0, x1)
new_compare(x0, x1, ty_Double)
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare1(x0, x1)
new_compare(x0, x1, ty_Float)
new_compare14(x0, x1, ty_Ordering)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_compare3(Pos(Succ(x0)), Pos(x1))
new_compare(x0, x1, ty_Ordering)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare5(x0, x1)
new_compare10(x0, x1)
new_compare3(Neg(Zero), Neg(Succ(x0)))
new_compare7(x0, x1, x2)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Zero)
new_merge00(x0, x1, x2, x3, LT, x4)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare2(:%(x0, x1), :%(x2, x3), ty_Integer)
new_compare14(x0, x1, ty_Float)
new_compare(x0, x1, app(ty_Ratio, x2))
new_primCmpNat1(Zero, Zero)
new_compare13(x0, x1, x2, x3, x4)
new_primCmpNat1(Succ(x0), Succ(x1))
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_compare14(x0, x1, app(ty_Maybe, x2))
new_merge_pairs0([], x0)
new_primPlusNat1(Zero, Succ(x0))
new_compare8(x0, x1, x2, x3)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), Zero)
new_compare(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_merge1(x0, [], :(x1, x2), x3)
new_compare14(x0, x1, ty_@0)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, ty_Char)
new_primCmpNat2(Zero, x0)
new_compare14(x0, x1, ty_Int)
new_compare3(Pos(Zero), Pos(Succ(x0)))
new_compare3(Neg(Zero), Neg(Zero))
new_compare(x0, x1, app(ty_[], x2))
new_compare11(x0, x1, x2)
new_compare0(x0, x1, x2, x3)
new_compare2(:%(x0, x1), :%(x2, x3), ty_Int)
new_primMulNat0(Succ(x0), Zero)
new_merge2(x0, [], x1)
new_primCmpNat0(x0, Zero)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare4(x0, x1)
new_compare14(x0, x1, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_compare3(Pos(Zero), Neg(Succ(x0)))
new_primCmpNat1(Succ(x0), Zero)
new_compare3(Neg(Zero), Pos(Succ(x0)))
new_compare3(Pos(Zero), Pos(Zero))
new_compare6(x0, x1)
new_compare3(Neg(Succ(x0)), Neg(x1))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpNat2(Succ(x0), x1)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Neg(x1))
new_compare3(Pos(Succ(x0)), Neg(x1))
new_compare3(Neg(Succ(x0)), Pos(x1))
new_compare14(x0, x1, ty_Integer)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_merge_pairs0(:(x0, []), x1)
new_primCmpNat1(Zero, Succ(x0))
new_compare(x0, x1, ty_@0)
new_primPlusNat1(Succ(x0), Succ(x1))
new_compare3(Neg(Zero), Pos(Zero))
new_compare3(Pos(Zero), Neg(Zero))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

case	cmp x y of
	GT	→ y : merge cmp (x : xs) ys
	_	→ x : merge cmp xs (y : ys)

merge0	y cmp x xs ys GT	= y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	= x : merge cmp xs (y : ys)